src/HOL/Tools/datatype_rep_proofs.ML
changeset 5553 ae42b36a50c2
parent 5303 22029546d109
child 5661 6ecb6ea25f19
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:16:06 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:17:14 1998 +0200
@@ -317,7 +317,7 @@
 
         (* prove characteristic equations *)
 
-        val rewrites = def_thms @ (map meta_eq rec_rewrites);
+        val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
         val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
           (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
 
@@ -381,7 +381,7 @@
 
         val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
 
-        val rewrites = map meta_eq iso_char_thms;
+        val rewrites = map mk_meta_eq iso_char_thms;
         val inj_thms' = map (fn r => r RS injD) inj_thms;
 
         val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
@@ -430,7 +430,7 @@
     fun prove_constr_rep_thm eqn =
       let
         val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
-        val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms)
+        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
       in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
         [resolve_tac inj_thms 1,
          rewrite_goals_tac rewrites,
@@ -524,7 +524,7 @@
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
             DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
-              (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
+              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
     val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;