src/HOL/Tools/BNF/bnf_lfp_compat.ML

   val datatype_compat: string list -> local_theory -> local_theory
   val datatype_compat_global: string list -> theory -> theory
   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 =
 struct
 

      |> co_datatypes Least_FP construct_lfp ((false, false), new_specs)
      |> Named_Target.exit
      |> 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"
     (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);