# HG changeset patch
# User blanchet
# Date 1420448081 -3600
# Node ID f5816b4d64893b1d82076bd2fc3004305c7c5361
# Parent  3a3e6e9c289f8afed6b9f9bdddf299c68f2926a2
tuning

diff -r 3a3e6e9c289f -r f5816b4d6489 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- 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 "|"
diff -r 3a3e6e9c289f -r f5816b4d6489 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- 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"