# HG changeset patch
# User wenzelm
# Date 1290970999 -3600
# Node ID d21aedaa91e7470a139d0aba868d7cc190c46728
# Parent  1d71a45590e42840b7baefd6c19acdd804c68b49
added Parse.literal_fact with proper inner_syntax markup (source position);
tuned;

diff -r 1d71a45590e4 -r d21aedaa91e7 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sun Nov 28 19:35:14 2010 +0100
+++ b/src/Pure/Isar/parse.ML	Sun Nov 28 20:03:19 2010 +0100
@@ -90,6 +90,7 @@
   val prop_group: string parser
   val term: string parser
   val prop: string parser
+  val literal_fact: string parser
   val propp: (string * string list) parser
   val termp: (string * string list) parser
   val target: xstring parser
@@ -315,14 +316,16 @@
 
 (* terms *)
 
-val trm = short_ident || long_ident || sym_ident || term_var || number || string;
+val tm = short_ident || long_ident || sym_ident || term_var || number || string;
 
-val term_group = group "term" trm;
-val prop_group = group "proposition" trm;
+val term_group = group "term" tm;
+val prop_group = group "proposition" tm;
 
 val term = inner_syntax term_group;
 val prop = inner_syntax prop_group;
 
+val literal_fact = inner_syntax (group "literal fact" alt_string);
+
 
 (* patterns *)
 
diff -r 1d71a45590e4 -r d21aedaa91e7 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sun Nov 28 19:35:14 2010 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 28 20:03:19 2010 +0100
@@ -61,7 +61,7 @@
 
 val xthm =
   Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
-  (Parse.alt_string >> Facts.Fact ||
+  (Parse.literal_fact >> Facts.Fact ||
     Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
 
 val xthms1 = Scan.repeat1 xthm;