# HG changeset patch
# User paulson
# Date 865511639 -7200
# Node ID 98f59f455d57be2a7957c423b2c7380c6831c842
# Parent  c0466958df5dd090cba33bb0cbb2058dee1762d3
freezeT now refers to Type.freeze_thaw

diff -r c0466958df5d -r 98f59f455d57 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jun 05 13:52:43 1997 +0200
+++ b/src/Pure/thm.ML	Thu Jun 05 13:53:59 1997 +0200
@@ -1086,7 +1086,7 @@
 
 (* Replace all TVars by new TFrees *)
 fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) =
-  let val prop' = Type.freeze prop
+  let val (prop',_) = Type.freeze_thaw prop
   in (*no fix_shyps*)
     Thm{sign = sign, 
         der = infer_derivs (FreezeT, [der]),