src/HOL/Tools/datatype_abs_proofs.ML

         in (defs @ [get_def thy' (Sign.base_name name)], thy')
         end) (([], thy), (hd descr) ~~ newTs ~~ case_names ~~
           (take (length newTs, reccomb_names)));
 
     val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
-      (map mk_meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
+      (map meta_eq primrec_thms)) (cterm_of (sign_of thy2) t)
         (fn _ => [rtac refl 1])))
           (DatatypeProp.make_cases new_type_names descr sorts thy2);
 
     val thy3 = Theory.add_trrules_i
       (DatatypeProp.make_case_trrules new_type_names descr) thy2

             val t::ts' = rev ts;
             val (_ $ (_ $ (_ $ (f $ _) $ _))) = hd (Logic.strip_imp_prems t);
             val cert = cterm_of (sign_of thy2);
             val distinct_lemma' = cterm_instantiate
               [(cert distinct_f, cert f)] distinct_lemma;
-            val rewrites = ord_defs @ (map mk_meta_eq case_thms)
+            val rewrites = ord_defs @ (map meta_eq case_thms)
           in
             (map (fn t => prove_goalw_cterm rewrites (cert t)
               (fn _ => [rtac refl 1])) (rev ts')) @ [standard distinct_lemma']
           end) ((hd descr) ~~ (DatatypeProp.make_distincts new_type_names
             descr sorts thy2) ~~ dist_rewrites ~~ case_thms)

         (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
           list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
             (size_names ~~ recTs ~~ def_names ~~ reccomb_names));
 
     val size_def_thms = map (get_axiom thy') def_names;
-    val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
+    val rewrites = size_def_thms @ map meta_eq primrec_thms;
 
     val size_thms = map (fn t => prove_goalw_cterm rewrites
       (cterm_of (sign_of thy') t) (fn _ => [rtac refl 1]))
         (DatatypeProp.make_size new_type_names descr sorts thy')