diff -r 82db9ad610b9 -r 8081087096ad src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -444,7 +444,7 @@
       |> map (maps (map_filter (find_rec_calls has_call)));
 
     fun is_only_old_datatype (Type (s, _)) =
-        is_some (Datatype_Data.get_info thy s) andalso not (is_new_datatype lthy0 s)
+        is_some (Old_Datatype_Data.get_info thy s) andalso not (is_new_datatype lthy0 s)
       | is_only_old_datatype _ = false;
 
     val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
@@ -561,8 +561,8 @@
   end
   handle OLD_PRIMREC () => old_primrec raw_fixes raw_specs lthy |>> apsnd single;
 
-val add_primrec = gen_primrec Primrec.add_primrec Specification.check_spec [];
-val add_primrec_cmd = gen_primrec Primrec.add_primrec_cmd Specification.read_spec;
+val add_primrec = gen_primrec Old_Primrec.add_primrec Specification.check_spec [];
+val add_primrec_cmd = gen_primrec Old_Primrec.add_primrec_cmd Specification.read_spec;
 
 fun add_primrec_global fixes specs =
   Named_Target.theory_init