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