src/Pure/Isar/parse.ML
changeset 40793 d21aedaa91e7
parent 40296 ac4d75f86d97
child 40800 330eb65c9469
     1.1 --- a/src/Pure/Isar/parse.ML	Sun Nov 28 19:35:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/parse.ML	Sun Nov 28 20:03:19 2010 +0100
     1.3 @@ -90,6 +90,7 @@
     1.4    val prop_group: string parser
     1.5    val term: string parser
     1.6    val prop: string parser
     1.7 +  val literal_fact: string parser
     1.8    val propp: (string * string list) parser
     1.9    val termp: (string * string list) parser
    1.10    val target: xstring parser
    1.11 @@ -315,14 +316,16 @@
    1.12  
    1.13  (* terms *)
    1.14  
    1.15 -val trm = short_ident || long_ident || sym_ident || term_var || number || string;
    1.16 +val tm = short_ident || long_ident || sym_ident || term_var || number || string;
    1.17  
    1.18 -val term_group = group "term" trm;
    1.19 -val prop_group = group "proposition" trm;
    1.20 +val term_group = group "term" tm;
    1.21 +val prop_group = group "proposition" tm;
    1.22  
    1.23  val term = inner_syntax term_group;
    1.24  val prop = inner_syntax prop_group;
    1.25  
    1.26 +val literal_fact = inner_syntax (group "literal fact" alt_string);
    1.27 +
    1.28  
    1.29  (* patterns *)
    1.30