--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:17:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 16:34:38 2014 +0200
@@ -28,6 +28,8 @@
val datatype_compat_cmd: string list -> local_theory -> local_theory
val add_datatype: nesting_preference -> Old_Datatype_Aux.spec list -> theory ->
string list * theory
+ val add_primrec: (binding * typ option * mixfix) list -> (Attrib.binding * term) list ->
+ local_theory -> (term list * thm list) * local_theory
end;
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -365,6 +367,8 @@
|> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names)))
end;
+val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
+
val _ =
Outer_Syntax.local_theory @{command_spec "datatype_compat"}
"register new-style datatypes as old-style datatypes"