src/HOL/Tools/Lifting/lifting_def.ML

     fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
         (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
       | 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
 
 (* This is not very cheap way of getting the rules but we have only few active