simplified syntax: Parse.term corresponds to Args.term etc.;
authorwenzelm
Tue May 24 15:53:16 2016 +0200 (2016-05-24)
changeset 631379553f11d67c4
parent 63136 fd11a538daac
child 63138 70f4d67235a0
simplified syntax: Parse.term corresponds to Args.term etc.;
src/Doc/Isar_Ref/Outer_Syntax.thy
src/Pure/Isar/parse.ML
     1.1 --- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:24:32 2016 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:53:16 2016 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4    @{rail \<open>
     1.5      @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
     1.6        @{syntax ident} | @{syntax longident} | @{syntax symident} |
     1.7 -      @{syntax nat}
     1.8 +      @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat}
     1.9    \<close>}
    1.10  \<close>
    1.11  
    1.12 @@ -278,12 +278,11 @@
    1.13    as \<^verbatim>\<open>=\<close> or \<^verbatim>\<open>+\<close>).
    1.14  
    1.15    @{rail \<open>
    1.16 -    @{syntax_def type}: @{syntax embedded} | @{syntax typefree} |
    1.17 -      @{syntax typevar}
    1.18 +    @{syntax_def type}: @{syntax embedded}
    1.19      ;
    1.20 -    @{syntax_def term}: @{syntax embedded} | @{syntax var}
    1.21 +    @{syntax_def term}: @{syntax embedded}
    1.22      ;
    1.23 -    @{syntax_def prop}: @{syntax term}
    1.24 +    @{syntax_def prop}: @{syntax embedded}
    1.25    \<close>}
    1.26  
    1.27    Positional instantiations are specified as a sequence of terms, or the
     2.1 --- a/src/Pure/Isar/parse.ML	Tue May 24 15:24:32 2016 +0200
     2.2 +++ b/src/Pure/Isar/parse.ML	Tue May 24 15:53:16 2016 +0200
     2.3 @@ -78,7 +78,6 @@
     2.4    val multi_arity: (string list * string list * string) parser
     2.5    val type_args: string list parser
     2.6    val type_args_constrained: (string * string option) list parser
     2.7 -  val typ_group: string parser
     2.8    val typ: string parser
     2.9    val mixfix: mixfix parser
    2.10    val mixfix': mixfix parser
    2.11 @@ -93,11 +92,9 @@
    2.12    val for_fixes: (binding * string option * mixfix) list parser
    2.13    val ML_source: Input.source parser
    2.14    val document_source: Input.source parser
    2.15 -  val term_group: string parser
    2.16 -  val prop_group: string parser
    2.17 +  val const: string parser
    2.18    val term: string parser
    2.19    val prop: string parser
    2.20 -  val const: string parser
    2.21    val literal_fact: string parser
    2.22    val propp: (string * string list) parser
    2.23    val termp: (string * string list) parser
    2.24 @@ -268,7 +265,8 @@
    2.25  
    2.26  val embedded =
    2.27    group (fn () => "embedded content")
    2.28 -    (short_ident || long_ident || sym_ident || number || string || cartouche);
    2.29 +    (cartouche || string || short_ident || long_ident || sym_ident ||
    2.30 +      term_var || type_ident || type_var || number);
    2.31  
    2.32  val text =
    2.33    group (fn () => "text")
    2.34 @@ -301,12 +299,7 @@
    2.35  
    2.36  (* types *)
    2.37  
    2.38 -val typ_group =
    2.39 -  group (fn () => "type")
    2.40 -    (short_ident || long_ident || sym_ident || type_ident || type_var || number ||
    2.41 -      string || cartouche);
    2.42 -
    2.43 -val typ = inner_syntax typ_group;
    2.44 +val typ = group (fn () => "type") (inner_syntax embedded);
    2.45  
    2.46  fun type_arguments arg =
    2.47    arg >> single ||
    2.48 @@ -393,13 +386,9 @@
    2.49  
    2.50  (* terms *)
    2.51  
    2.52 -val term_group = group (fn () => "term") (term_var || embedded);
    2.53 -val prop_group = group (fn () => "proposition") (term_var || embedded);
    2.54 -
    2.55 -val term = inner_syntax term_group;
    2.56 -val prop = inner_syntax prop_group;
    2.57 -
    2.58  val const = group (fn () => "constant") (inner_syntax embedded);
    2.59 +val term = group (fn () => "term") (inner_syntax embedded);
    2.60 +val prop = group (fn () => "proposition") (inner_syntax embedded);
    2.61  
    2.62  val literal_fact = inner_syntax (group (fn () => "literal fact") (alt_string || cartouche));
    2.63