src/Pure/Isar/outer_parse.ML
changeset 17756 d4a35f82fbb4
parent 17358 5746c9bd4356
child 18037 1095d2213b9d
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Oct 04 16:47:40 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Oct 04 19:01:37 2005 +0200
     1.3 @@ -303,7 +303,7 @@
     1.4  
     1.5  fun thm_name s = name -- opt_attribs --| $$$ s;
     1.6  fun opt_thm_name s =
     1.7 -  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);;
     1.8 +  Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);
     1.9  
    1.10  val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
    1.11  val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));