--- 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