src/Pure/Isar/parse_spec.ML
changeset 40793 d21aedaa91e7
parent 36955 226fb165833e
child 40800 330eb65c9469
     1.1 --- a/src/Pure/Isar/parse_spec.ML	Sun Nov 28 19:35:14 2010 +0100
     1.2 +++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 28 20:03:19 2010 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4  
     1.5  val xthm =
     1.6    Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
     1.7 -  (Parse.alt_string >> Facts.Fact ||
     1.8 +  (Parse.literal_fact >> Facts.Fact ||
     1.9      Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    1.10  
    1.11  val xthms1 = Scan.repeat1 xthm;