diff -r 82db9ad610b9 -r 8081087096ad src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -585,7 +585,7 @@
       | rename t _ = t
 
     val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
-    val new_names = Datatype_Prop.make_tnames (all_typs fixed_def_t)
+    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
   in
     rename term new_names
   end