# HG changeset patch
# User wenzelm
# Date 1529584184 -7200
# Node ID fb6afa538b04eb46e82f54e2f586639efa05fbc1
# Parent  27be5b4cb80d10937156334999b8281d32b237b3
more uniform syntax;

diff -r 27be5b4cb80d -r fb6afa538b04 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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} |
diff -r 27be5b4cb80d -r fb6afa538b04 src/Pure/Thy/document_antiquotations.ML
--- 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)