# HG changeset patch # User blanchet # Date 1411126900 -7200 # Node ID f0c51576964af1eeac6f1f8ce2e4efb14c8325a8 # Parent dafe52a76ae7d977952f09a5c578e22b32caaeb3 more honest 'primcorec' -- don't parse a theorem name that is then ignored diff -r dafe52a76ae7 -r f0c51576964a src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 19 13:38:21 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 19 13:41:40 2014 +0200 @@ -1453,8 +1453,9 @@ (Parse.reserved "sequential" >> K Sequential_Option || Parse.reserved "exhaustive" >> K Exhaustive_Option) +(* FIXME: should use "Parse_Spec.spec" instead of "Parse.prop" and honor binding *) val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|" - (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const))); + ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const))); val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"} "define primitive corecursive functions"