Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

improper bug for meta-args-parser

This commit is contained in:
Burkhart Wolff 2019-06-29 11:20:05 +02:00
parent a65f0b7e09
commit b439fbb90b
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
patches/thy_output.ML
View File

@ -388,10 +388,10 @@ fun present_thy options thy (segments: segment list) =
pred keywords (Token.content_of tok)))
-- (Document_Source.annotation |--
(Parse.!!!!
( (!meta_args_parser_hook thy)
( (Document_Source.improper |-- (!meta_args_parser_hook thy))
-- ( (Document_Source.improper -- locale -- Document_Source.improper)
|-- Parse.document_source )
--| Document_Source.improper_end)
|-- Parse.document_source )
--| Document_Source.improper_end)
)
)