diff -r a2ba381607fb -r 3831312eb476 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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"