changeset 63352 | 4eaf35781b23 |
parent 63285 | e9c777bfd78c |
child 67450 | b0ae74b86ef3 |
--- a/src/Pure/Isar/parse_spec.ML Wed Jun 22 16:04:03 2016 +0200 +++ b/src/Pure/Isar/parse_spec.ML Thu Jun 23 11:01:14 2016 +0200 @@ -46,7 +46,7 @@ fun opt_thm_name s = Scan.optional ((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s) - Attrib.empty_binding; + Binding.empty_atts; val simple_spec = opt_thm_name ":" -- Parse.prop; val simple_specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;