# 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"