--- a/src/Doc/Isar_Ref/Document_Preparation.thy Thu Jun 21 14:17:57 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Thu Jun 21 14:29:44 2018 +0200
@@ -167,7 +167,7 @@
@{syntax_def antiquotation_body}:
(@@{antiquotation text} | @@{antiquotation cartouche} | @@{antiquotation theory_text})
options @{syntax text} |
- @@{antiquotation theory} options @{syntax name} |
+ @@{antiquotation theory} options @{syntax embedded} |
@@{antiquotation thm} options styles @{syntax thms} |
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
--- a/src/Pure/Thy/document_antiquotations.ML Thu Jun 21 14:17:57 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Thu Jun 21 14:29:44 2018 +0200
@@ -82,7 +82,7 @@
basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
- basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.name)) pretty_theory #>
+ basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #>
basic_entities \<^binding>\<open>prf\<close> Attrib.thms (pretty_prf false) #>
basic_entities \<^binding>\<open>full_prf\<close> Attrib.thms (pretty_prf true) #>
Document_Antiquotation.setup \<^binding>\<open>thm\<close> (Term_Style.parse -- Attrib.thms)