--- a/src/HOL/Import/shuffler.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Sat Nov 21 15:49:29 2009 +0100
@@ -294,7 +294,7 @@
fun eta_contract thy assumes origt =
let
val (typet,Tinst) = freeze_thaw_term origt
- val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+ val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
val final = inst_tfrees thy Tinst o thaw
val t = #1 (Logic.dest_equals (prop_of init))
val _ =
@@ -357,7 +357,7 @@
fun eta_expand thy assumes origt =
let
val (typet,Tinst) = freeze_thaw_term origt
- val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+ val (init,thaw) = Drule.legacy_freeze_thaw (reflexive (cterm_of thy typet))
val final = inst_tfrees thy Tinst o thaw
val t = #1 (Logic.dest_equals (prop_of init))
val _ =
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sat Nov 21 15:49:29 2009 +0100
@@ -365,7 +365,7 @@
let
val prop = Thm.prop_of thm;
val _ $ (_ $ ((S as Const (_, Type (_, [U, _]))) $ _ )) $
- (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
+ (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.legacy_freeze prop;
val used = OldTerm.add_term_tfree_names (a, []);
fun mk_thm i =
--- a/src/HOL/Tools/TFL/post.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sat Nov 21 15:49:29 2009 +0100
@@ -27,7 +27,7 @@
* have a tactic directly applied to them.
*--------------------------------------------------------------------------*)
fun termination_goals rules =
- map (Type.freeze o HOLogic.dest_Trueprop)
+ map (Type.legacy_freeze o HOLogic.dest_Trueprop)
(fold_rev (union (op aconv) o prems_of) rules []);
(*---------------------------------------------------------------------------
--- a/src/HOL/Tools/meson.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/meson.ML Sat Nov 21 15:49:29 2009 +0100
@@ -665,7 +665,7 @@
(*Converting one theorem from a disjunction to a meta-level clause*)
fun make_meta_clause th =
- let val (fth,thaw) = Drule.freeze_thaw_robust th
+ let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
in
(zero_var_indexes o Thm.varifyT o thaw 0 o
negated_asm_of_head o make_horn resolution_clause_rules) fth
--- a/src/HOL/Tools/old_primrec.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/old_primrec.ML Sat Nov 21 15:49:29 2009 +0100
@@ -45,7 +45,7 @@
let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
val (env, _) = fold unify rec_consts (Vartab.empty, i');
- val subst = Type.freeze o map_types (Envir.norm_type env)
+ val subst = Type.legacy_freeze o map_types (Envir.norm_type env)
in (map subst cs', map subst intr_ts')
end) handle Type.TUNIFY =>
--- a/src/HOL/Tools/res_axioms.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sat Nov 21 15:49:29 2009 +0100
@@ -29,8 +29,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if ! trace then tracing (msg ()) else ();
-(* FIXME legacy *)
-fun freeze_thm th = #1 (Drule.freeze_thaw th);
+fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
fun type_has_empty_sort (TFree (_, [])) = true
| type_has_empty_sort (TVar (_, [])) = true
--- a/src/Pure/Proof/extraction.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Nov 21 15:49:29 2009 +0100
@@ -310,7 +310,7 @@
val vars' = filter_out (fn v =>
member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
val T = etype_of thy' vs [] prop;
- val (T', thw) = Type.freeze_thaw_type
+ val (T', thw) = Type.legacy_freeze_thaw_type
(if T = nullT then nullT else map fastype_of vars' ---> T);
val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
val r' = freeze_thaw (condrew thy' eqns
@@ -720,8 +720,8 @@
NONE =>
let
val corr_prop = Reconstruct.prop_of prf;
- val ft = Type.freeze t;
- val fu = Type.freeze u;
+ val ft = Type.legacy_freeze t;
+ val fu = Type.legacy_freeze u;
val (def_thms, thy') = if t = nullt then ([], thy) else
thy
|> Sign.add_consts_i [(Binding.qualified_name (extr_name s vs), fastype_of ft, NoSyn)]
--- a/src/Pure/drule.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/drule.ML Sat Nov 21 15:49:29 2009 +0100
@@ -21,8 +21,8 @@
val forall_elim_list: cterm list -> thm -> thm
val gen_all: thm -> thm
val lift_all: cterm -> thm -> thm
- val freeze_thaw: thm -> thm * (thm -> thm)
- val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
+ val legacy_freeze_thaw: thm -> thm * (thm -> thm)
+ val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
@@ -325,7 +325,7 @@
reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.
Similar code in type/freeze_thaw*)
-fun freeze_thaw_robust th =
+fun legacy_freeze_thaw_robust th =
let val fth = Thm.freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
@@ -346,9 +346,8 @@
end;
(*Basic version of the function above. No option to rename Vars apart in thaw.
- The Frees created from Vars have nice names. FIXME: does not check for
- clashes with variables in the assumptions, so delete and use freeze_thaw_robust instead?*)
-fun freeze_thaw th =
+ The Frees created from Vars have nice names.*)
+fun legacy_freeze_thaw th =
let val fth = Thm.freezeT th
val thy = Thm.theory_of_thm fth
val {prop, tpairs, ...} = rep_thm fth
--- a/src/Pure/thm.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/thm.ML Sat Nov 21 15:49:29 2009 +0100
@@ -1267,7 +1267,7 @@
fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
let
val prop1 = attach_tpairs tpairs prop;
- val prop2 = Type.freeze prop1;
+ val prop2 = Type.legacy_freeze prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
in
Thm (deriv_rule1 (Pt.freezeT prop1) der,
--- a/src/Pure/type.ML Sat Nov 21 14:03:36 2009 +0100
+++ b/src/Pure/type.ML Sat Nov 21 15:49:29 2009 +0100
@@ -44,10 +44,10 @@
val strip_sorts: typ -> typ
val no_tvars: typ -> typ
val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
- val freeze_thaw_type: typ -> typ * (typ -> typ)
- val freeze_type: typ -> typ
- val freeze_thaw: term -> term * (term -> term)
- val freeze: term -> term
+ val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
+ val legacy_freeze_type: typ -> typ
+ val legacy_freeze_thaw: term -> term * (term -> term)
+ val legacy_freeze: term -> term
(*matching and unification*)
exception TYPE_MATCH
@@ -277,17 +277,16 @@
in
-(*this sort of code could replace unvarifyT*)
-fun freeze_thaw_type T =
+fun legacy_freeze_thaw_type T =
let
val used = OldTerm.add_typ_tfree_names (T, [])
and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
val (alist, _) = List.foldr new_name ([], used) tvars;
in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
-val freeze_type = #1 o freeze_thaw_type;
+val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
-fun freeze_thaw t =
+fun legacy_freeze_thaw t =
let
val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
@@ -299,7 +298,7 @@
map_types (map_type_tfree (thaw_one (map swap alist)))))
end;
-val freeze = #1 o freeze_thaw;
+val legacy_freeze = #1 o legacy_freeze_thaw;
end;