--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Feb 17 13:31:42 2014 +0100
@@ -1373,4 +1373,23 @@
| _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
goalss)) ooo add_primcorec_ursive_cmd true;
+val primcorec_option_parser = Parse.group (fn () => "option")
+ (Parse.reserved "sequential" >> K Sequential_Option
+ || Parse.reserved "exhaustive" >> K Exhaustive_Option)
+
+val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
+ (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
+
+val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
+ "define primitive corecursive functions"
+ ((Scan.optional (@{keyword "("} |--
+ Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
+ (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
+
+val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
+ "define primitive corecursive functions"
+ ((Scan.optional (@{keyword "("} |--
+ Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) --
+ (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
+
end;