author | paulson |
Thu, 05 Jun 1997 13:53:59 +0200 | |
changeset 3410 | 98f59f455d57 |
parent 3409 | c0466958df5d |
child 3411 | 163f8f4a42d7 |
src/Pure/thm.ML | file | annotate | diff | comparison | revisions |
--- 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]),