src/Doc/Isar_Ref/Outer_Syntax.thy
changeset 63139 d905741a80e8
parent 63138 70f4d67235a0
child 63140 0644c2e5a989
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 16:03:03 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 16:13:59 2016 +0200
@@ -238,7 +238,7 @@
   Isabelle/Isar commands.
 
   @{rail \<open>
-    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax name}
+    @{syntax_def text}: @{syntax embedded} | @{syntax verbatim}
     ;
     @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
   \<close>}