--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon May 03 20:13:36 2010 +0200
@@ -48,7 +48,7 @@
fun atomize_thm thm =
let
- val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
+ val thm' = Thm.legacy_freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
val thm'' = Object_Logic.atomize (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
--- a/src/HOL/Tools/TFL/post.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/TFL/post.ML Mon May 03 20:13:36 2010 +0200
@@ -141,7 +141,7 @@
fun simplify_defn strict thy cs ss congs wfs id pats def0 =
let
val ctxt = ProofContext.init_global thy
- val def = Thm.freezeT def0 RS meta_eq_to_obj_eq
+ val def = Thm.legacy_freezeT def0 RS meta_eq_to_obj_eq
val {rules,rows,TCs,full_pats_TCs} =
Prim.post_definition congs (thy, (def,pats))
val {lhs=f,rhs} = S.dest_eq (concl def)
--- a/src/HOL/Tools/TFL/rules.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Mon May 03 20:13:36 2010 +0200
@@ -136,7 +136,7 @@
(* freezeT expensive! *)
fun UNDISCH thm =
- let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.freezeT thm))))
+ let val tm = D.mk_prop (#1 (D.dest_imp (cconcl (Thm.legacy_freezeT thm))))
in Thm.implies_elim (thm RS mp) (ASSUME tm) end
handle U.ERR _ => raise RULES_ERR "UNDISCH" ""
| THM _ => raise RULES_ERR "UNDISCH" "";
@@ -265,7 +265,7 @@
| DL th (th1::rst) =
let val tm = #2(D.dest_disj(D.drop_prop(cconcl th)))
in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
- in DL (Thm.freezeT disjth) (organize eq tml thl)
+ in DL (Thm.legacy_freezeT disjth) (organize eq tml thl)
end;
--- a/src/HOL/Tools/TFL/tfl.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Mon May 03 20:13:36 2010 +0200
@@ -541,7 +541,7 @@
thy
|> PureThy.add_defs false
[Thm.no_attributes (Binding.name (fid ^ "_def"), defn)]
- val def = Thm.freezeT def0;
+ val def = Thm.legacy_freezeT def0;
val dummy =
if !trace then writeln ("DEF = " ^ Display.string_of_thm_global theory def)
else ()
--- a/src/HOL/Tools/choice_specification.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML Mon May 03 20:13:36 2010 +0200
@@ -79,7 +79,7 @@
end
fun add_specification axiomatic cos arg =
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.legacy_freezeT
|> proc_exprop axiomatic cos
|> apsnd Drule.export_without_context
@@ -217,7 +217,7 @@
then writeln "specification"
else ()
in
- arg |> apsnd Thm.freezeT
+ arg |> apsnd Thm.legacy_freezeT
|> process_all (zip3 alt_names rew_imps frees)
end
--- a/src/Pure/Isar/code.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/Pure/Isar/code.ML Mon May 03 20:13:36 2010 +0200
@@ -778,7 +778,7 @@
val _ = if c = const_abs_eqn thy abs_thm then ()
else error ("Wrong head of abstract code equation,\nexpected constant "
^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
- in Abstract (Thm.freezeT abs_thm, tyco) end;
+ in Abstract (Thm.legacy_freezeT abs_thm, tyco) end;
fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
let
--- a/src/Pure/drule.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/Pure/drule.ML Mon May 03 20:13:36 2010 +0200
@@ -307,7 +307,7 @@
Similar code in type/freeze_thaw*)
fun legacy_freeze_thaw_robust th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
@@ -329,7 +329,7 @@
(*Basic version of the function above. No option to rename Vars apart in thaw.
The Frees created from Vars have nice names.*)
fun legacy_freeze_thaw th =
- let val fth = Thm.freezeT th
+ let val fth = Thm.legacy_freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
in
--- a/src/Pure/thm.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/Pure/thm.ML Mon May 03 20:13:36 2010 +0200
@@ -140,7 +140,7 @@
val strip_shyps: thm -> thm
val unconstrainT: ctyp -> thm -> thm
val unconstrain_allTs: thm -> thm
- val freezeT: thm -> thm
+ val legacy_freezeT: thm -> thm
val assumption: int -> thm -> thm Seq.seq
val eq_assumption: int -> thm -> thm
val rotate_rule: int -> int -> thm -> thm
@@ -1261,8 +1261,8 @@
val varifyT_global = #2 o varifyT_global' [];
-(* Replace all TVars by new TFrees *)
-fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
+(* Replace all TVars by TFrees that are often new *)
+fun legacy_freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
let
val prop1 = attach_tpairs tpairs prop;
val prop2 = Type.legacy_freeze prop1;
--- a/src/Tools/nbe.ML Mon May 03 16:26:47 2010 +0200
+++ b/src/Tools/nbe.ML Mon May 03 20:13:36 2010 +0200
@@ -105,14 +105,14 @@
|> Drule.cterm_rule Thm.varifyT_global
|> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
(((v, 0), sort), TFree (v, sort'))) vs, []))
- |> Drule.cterm_rule Thm.freezeT
+ |> Drule.cterm_rule Thm.legacy_freezeT
|> conv
|> Thm.varifyT_global
|> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
|> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
(((v, 0), []), TVar ((v, 0), sort))) vs, [])
|> strip_of_class
- |> Thm.freezeT
+ |> Thm.legacy_freezeT
end;
fun lift_triv_classes_rew thy rew t =