src/HOL/Tools/datatype_rep_proofs.ML
changeset 5553 ae42b36a50c2
parent 5303 22029546d109
child 5661 6ecb6ea25f19
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:16:06 1998 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Sep 24 17:17:14 1998 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4  
     1.5          (* prove characteristic equations *)
     1.6  
     1.7 -        val rewrites = def_thms @ (map meta_eq rec_rewrites);
     1.8 +        val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
     1.9          val char_thms' = map (fn eqn => prove_goalw_cterm rewrites
    1.10            (cterm_of (sign_of thy') eqn) (fn _ => [rtac refl 1])) eqns;
    1.11  
    1.12 @@ -381,7 +381,7 @@
    1.13  
    1.14          val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
    1.15  
    1.16 -        val rewrites = map meta_eq iso_char_thms;
    1.17 +        val rewrites = map mk_meta_eq iso_char_thms;
    1.18          val inj_thms' = map (fn r => r RS injD) inj_thms;
    1.19  
    1.20          val inj_thm = prove_goalw_cterm [] (cterm_of (sign_of thy5)
    1.21 @@ -430,7 +430,7 @@
    1.22      fun prove_constr_rep_thm eqn =
    1.23        let
    1.24          val inj_thms = map (fn (r, _) => r RS inj_onD) newT_iso_inj_thms;
    1.25 -        val rewrites = constr_defs @ (map (meta_eq o #2) newT_iso_axms)
    1.26 +        val rewrites = constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    1.27        in prove_goalw_cterm [] (cterm_of (sign_of thy5) eqn) (fn _ =>
    1.28          [resolve_tac inj_thms 1,
    1.29           rewrite_goals_tac rewrites,
    1.30 @@ -524,7 +524,7 @@
    1.31             [REPEAT (eresolve_tac Abs_inverse_thms 1),
    1.32              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    1.33              DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
    1.34 -              (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
    1.35 +              (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    1.36  
    1.37      val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
    1.38