# HG changeset patch
# User wenzelm
# Date 1464099239 -7200
# Node ID d905741a80e85d559df6524f36f28598e0106383
# Parent  70f4d67235a0471b93d0bbf50c80f33b4df86429
simplified syntax;

diff -r 70f4d67235a0 -r d905741a80e8 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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>}
diff -r 70f4d67235a0 -r d905741a80e8 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue May 24 16:03:03 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Tue May 24 16:13:59 2016 +0200
@@ -268,9 +268,7 @@
     (cartouche || string || short_ident || long_ident || sym_ident ||
       term_var || type_ident || type_var || number);
 
-val text =
-  group (fn () => "text")
-    (short_ident || long_ident || sym_ident || number || string || verbatim || cartouche);
+val text = group (fn () => "text") (embedded || verbatim);
 
 val path = group (fn () => "file name/path specification") name;