equal
deleted
inserted
replaced
1049 |
1049 |
1050 (* Replace all TVars by new TFrees *) |
1050 (* Replace all TVars by new TFrees *) |
1051 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1051 fun freezeT(Thm{sign_ref,der,maxidx,shyps,hyps,tpairs,prop}) = |
1052 let |
1052 let |
1053 val prop1 = attach_tpairs tpairs prop; |
1053 val prop1 = attach_tpairs tpairs prop; |
1054 val (prop2, _) = Type.freeze_thaw prop1; |
1054 val prop2 = Type.freeze prop1; |
1055 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1055 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2) |
1056 in (*no fix_shyps*) |
1056 in (*no fix_shyps*) |
1057 Thm{sign_ref = sign_ref, |
1057 Thm{sign_ref = sign_ref, |
1058 der = Pt.infer_derivs' (Pt.freezeT prop1) der, |
1058 der = Pt.infer_derivs' (Pt.freezeT prop1) der, |
1059 maxidx = maxidx_of_term prop2, |
1059 maxidx = maxidx_of_term prop2, |