--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jan 05 09:54:40 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jan 05 09:54:41 2015 +0100
@@ -1484,10 +1484,10 @@
| _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
goalss)) ooo add_primcorec_ursive_cmd true;
-val primcorec_option_parser = Parse.group (fn () => "option")
+val primcorec_option_parser = Parse.group (K "option")
(Parse.reserved "sequential" >> K Sequential_Option
- || Parse.reserved "exhaustive" >> K Exhaustive_Option
- || Parse.reserved "transfer" >> K Transfer_Option)
+ || Parse.reserved "exhaustive" >> K Exhaustive_Option
+ || Parse.reserved "transfer" >> K Transfer_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 "|"
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 05 09:54:40 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Jan 05 09:54:41 2015 +0100
@@ -658,9 +658,9 @@
#> add_primrec fixes specs
##> Local_Theory.exit_global;
-val primrec_option_parser = Parse.group (fn () => "option")
+val primrec_option_parser = Parse.group (K "option")
(Parse.reserved "nonexhaustive" >> K Nonexhaustive_Option
- || Parse.reserved "transfer" >> K Transfer_Option)
+ || Parse.reserved "transfer" >> K Transfer_Option);
val _ = Outer_Syntax.local_theory @{command_spec "primrec"}
"define primitive recursive functions"