changeset 6398 | e6f0c192ef88 |
parent 6372 | 44b104595441 |
child 6430 | 69400c97d3bf |
--- a/src/Pure/Isar/outer_parse.ML Wed Mar 17 17:20:36 1999 +0100 +++ b/src/Pure/Isar/outer_parse.ML Wed Mar 17 18:01:41 1999 +0100 @@ -241,7 +241,7 @@ val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]"); val opt_attribs = Scan.optional attribs []; -fun thm_name s = name -- (!!! (opt_attribs --| $$$ s)); +fun thm_name s = name -- opt_attribs --| $$$ s; fun opt_thm_name s = Scan.optional (thm_name s) ("", []); val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));