src/Doc/Implementation/Prelim.thy
changeset 62969 9f394a16c557
parent 61854 38b049cd3aad
child 67146 909dcdec2122
--- a/src/Doc/Implementation/Prelim.thy	Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 13 18:01:05 2016 +0200
@@ -142,9 +142,9 @@
   \end{matharray}
 
   @{rail \<open>
-  @@{ML_antiquotation theory} nameref?
+  @@{ML_antiquotation theory} name?
   ;
-  @@{ML_antiquotation theory_context} nameref
+  @@{ML_antiquotation theory_context} name
   \<close>}
 
   \<^descr> \<open>@{theory}\<close> refers to the background theory of the current context --- as