Type.freeze;

--- a/TFL/post.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/TFL/post.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -45,7 +45,7 @@
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 fun termination_goals rules =
-    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
+    map (Type.freeze o HOLogic.dest_Trueprop)
       (foldr (fn (th,A) => union_term (prems_of th, A)) [] rules);
 
 (*---------------------------------------------------------------------------

--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -388,8 +388,8 @@
     fun mk_funs_inv thm =
       let
         val {sign, prop, ...} = rep_thm thm;
-        val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
-          (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
+        val _ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
+          (_ $ (_ $ (r $ (a $ _)) $ _)) = Type.freeze prop;
         val used = add_term_tfree_names (a, []);
 
         fun mk_thm i =

--- a/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -193,8 +193,7 @@
           (env, (replicate (length consts) cT) ~~ consts)
       end;
     val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
-    val subst = fst o Type.freeze_thaw o
-      (map_term_types (Envir.norm_type env))
+    val subst = Type.freeze o map_term_types (Envir.norm_type env)
 
   in (map subst cs', map subst intr_ts')
   end) handle Type.TUNIFY =>

--- a/src/Pure/Proof/extraction.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -748,8 +748,8 @@
          NONE =>
            let
              val corr_prop = Reconstruct.prop_of prf;
-             val ft = fst (Type.freeze_thaw t);
-             val fu = fst (Type.freeze_thaw u);
+             val ft = Type.freeze t;
+             val fu = Type.freeze u;
              val thy' = if t = nullt then thy else thy |>
                Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |>
                fst o PureThy.add_defs_i false [((extr_name s vs ^ "_def",

--- a/src/Pure/thm.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/src/Pure/thm.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -1051,7 +1051,7 @@
 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) =
   let
     val prop1 = attach_tpairs tpairs prop;
-    val (prop2, _) = Type.freeze_thaw prop1;
+    val prop2 = Type.freeze prop1;
     val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2)
   in (*no fix_shyps*)
     Thm{sign_ref = sign_ref,