--- a/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML Wed Aug 12 16:20:49 1998 +0200
@@ -26,7 +26,7 @@
local
val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))];
- val rew = mk_meta_eq pair_eta_expand;
+ val rew = meta_eq pair_eta_expand;
fun proc _ _ (Abs _) = Some rew
| proc _ _ _ = None;
--- a/src/HOL/Prod.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Prod.ML Wed Aug 12 16:20:49 1998 +0200
@@ -153,7 +153,7 @@
local
val split_eta_pat = Thm.read_cterm (sign_of thy)
("split (%x. split (%y. f x y))", HOLogic.termTVar);
- val split_eta_meta_eq = standard (mk_meta_eq cond_split_eta);
+ val split_eta_meta_eq = standard (meta_eq cond_split_eta);
fun Pair_pat 0 (Bound 0) = true
| Pair_pat k (Const ("Pair", _) $ Bound m $ t) =
m = k andalso Pair_pat (k-1) t
@@ -176,7 +176,7 @@
val ct = cterm_of (sign_of thy) (HOLogic.mk_Trueprop
(HOLogic.mk_eq (atom_fun s,fvar)));
val ss = HOL_basic_ss addsimps [cond_split_eta];
- in Some (mk_meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
+ in Some (meta_eq (prove_goalw_cterm [] ct (K [simp_tac ss 1]))) end)
| None => None)
| proc _ _ _ = None;
@@ -435,7 +435,7 @@
Cannot use this rule directly -- it loops!*)
local
val unit_pat = Thm.cterm_of (sign_of thy) (Free ("x", HOLogic.unitT));
- val unit_meta_eq = standard (mk_meta_eq unit_eq);
+ val unit_meta_eq = standard (meta_eq unit_eq);
fun proc _ _ t =
if HOLogic.is_unit t then None
else Some unit_meta_eq;
--- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Aug 12 16:20:49 1998 +0200
@@ -329,7 +329,7 @@
(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);
@@ -399,7 +399,7 @@
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']
@@ -490,7 +490,7 @@
(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]))
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Aug 12 16:20:49 1998 +0200
@@ -317,7 +317,7 @@
(* prove characteristic equations *)
- val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
+ val rewrites = def_thms @ (map 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 mk_meta_eq iso_char_thms;
+ val rewrites = map 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 (mk_meta_eq o #2) newT_iso_axms)
+ val rewrites = constr_defs @ (map (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 mk_meta_eq iso_char_thms))))]);
+ (prems ~~ (constr_defs @ (map meta_eq iso_char_thms))))]);
val thy7 = PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] thy6;
--- a/src/HOL/Tools/inductive_package.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML Wed Aug 12 16:20:49 1998 +0200
@@ -341,14 +341,14 @@
HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
nth_elem (find_index_eq c cs, preds)))))
(fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
- (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+ (map meta_eq [sum_case_Inl, sum_case_Inr]),
rtac refl 1])) cs;
val induct = prove_goalw_cterm [] (cterm_of sign
(Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
[rtac (impI RS allI) 1,
DETERM (etac (mono RS (fp_def RS def_induct)) 1),
- rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
+ rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)),
fold_goals_tac rec_sets_defs,
(*This CollectE and disjE separates out the introduction rules*)
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
@@ -356,7 +356,7 @@
some premise involves disjunction.*)
REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE]
ORELSE' hyp_subst_tac)),
- rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+ rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
EVERY (map (fn prem =>
DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
@@ -366,7 +366,7 @@
REPEAT (EVERY
[REPEAT (resolve_tac [conjI, impI] 1),
TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
- rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
+ rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
atac 1])])
in standard (split_rule (induct RS lemma))
@@ -451,7 +451,7 @@
prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
val raw_induct = if no_ind then TrueI else
if coind then standard (rule_by_tactic
- (rewrite_tac [mk_meta_eq vimage_Un] THEN
+ (rewrite_tac [meta_eq vimage_Un] THEN
fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
else
prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
--- a/src/HOL/Tools/primrec_package.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/Tools/primrec_package.ML Wed Aug 12 16:20:49 1998 +0200
@@ -221,7 +221,7 @@
(if eq_set (names1, names2) then Theory.add_defs_i defs'
else primrec_err ("functions " ^ commas names2 ^
"\nare not mutually recursive"));
- val rewrites = (map mk_meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
+ val rewrites = (map meta_eq rec_rewrites) @ (map (get_axiom thy' o fst) defs');
val _ = writeln ("Proving equations for primrec function(s)\n" ^
commas names1 ^ " ...");
val char_thms = map (fn t => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
--- a/src/HOL/arith_data.ML Wed Aug 12 16:16:49 1998 +0200
+++ b/src/HOL/arith_data.ML Wed Aug 12 16:20:49 1998 +0200
@@ -56,7 +56,7 @@
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun prove_conv expand_tac norm_tac sg (t, u) =
- mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
+ meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u)))
(K [expand_tac, norm_tac]))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
(string_of_cterm (cterm_of sg (mk_eqv (t, u)))));