# HG changeset patch
# User wenzelm
# Date 1464097996 -7200
# Node ID 9553f11d67c46e3eedb7f98dac93a8f766cbf6d6
# Parent  fd11a538daac7b2245d93eaad7bff94ccc2a0259
simplified syntax: Parse.term corresponds to Args.term etc.;

diff -r fd11a538daac -r 9553f11d67c4 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:24:32 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:53:16 2016 +0200
@@ -222,7 +222,7 @@
   @{rail \<open>
     @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
       @{syntax ident} | @{syntax longident} | @{syntax symident} |
-      @{syntax nat}
+      @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat}
   \<close>}
 \<close>
 
@@ -278,12 +278,11 @@
   as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
 
   @{rail \<open>
-    @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
-      @{syntax typevar}
+    @{syntax_def type}: @{syntax embedded}
     ;
-    @{syntax_def term}: @{syntax embedded} | @{syntax var}
+    @{syntax_def term}: @{syntax embedded}
     ;
-    @{syntax_def prop}: @{syntax term}
+    @{syntax_def prop}: @{syntax embedded}
   \<close>}
 
   Positional instantiations are specified as a sequence of terms, or the
diff -r fd11a538daac -r 9553f11d67c4 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue May 24 15:24:32 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Tue May 24 15:53:16 2016 +0200
@@ -78,7 +78,6 @@
   val multi_arity: (string list * string list * string) parser
   val type_args: string list parser
   val type_args_constrained: (string * string option) list parser
-  val typ_group: string parser
   val typ: string parser
   val mixfix: mixfix parser
   val mixfix': mixfix parser
@@ -93,11 +92,9 @@
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: Input.source parser
   val document_source: Input.source parser
-  val term_group: string parser
-  val prop_group: string parser
+  val const: string parser
   val term: string parser
   val prop: string parser
-  val const: string parser
   val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
@@ -268,7 +265,8 @@
 
 val embedded =
   group (fn () => "embedded content")
-    (short_ident || long_ident || sym_ident || number || string || cartouche);
+    (cartouche || string || short_ident || long_ident || sym_ident ||
+      term_var || type_ident || type_var || number);
 
 val text =
   group (fn () => "text")
@@ -301,12 +299,7 @@
 
 (* types *)
 
-val typ_group =
-  group (fn () => "type")
-    (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
-      string || cartouche);
-
-val typ = inner_syntax typ_group;
+val typ = group (fn () => "type") (inner_syntax embedded);
 
 fun type_arguments arg =
   arg >> single ||
@@ -393,13 +386,9 @@
 
 (* terms *)
 
-val term_group = group (fn () => "term") (term_var || embedded);
-val prop_group = group (fn () => "proposition") (term_var || embedded);
-
-val term = inner_syntax term_group;
-val prop = inner_syntax prop_group;
-
 val const = group (fn () => "constant") (inner_syntax embedded);
+val term = group (fn () => "term") (inner_syntax embedded);
+val prop = group (fn () => "proposition") (inner_syntax embedded);
 
 val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));