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