1956 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = |
1956 fun legacy_freezeT (Thm (der, {cert, constraints, shyps, hyps, tpairs, prop, ...})) = |
1957 let |
1957 let |
1958 val prop1 = attach_tpairs tpairs prop; |
1958 val prop1 = attach_tpairs tpairs prop; |
1959 val prop2 = Type.legacy_freeze prop1; |
1959 val prop2 = Type.legacy_freeze prop1; |
1960 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1960 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1961 in |
1961 fun prf p = Proofterm.legacy_freezeT prop1 p; |
1962 Thm (deriv_rule1 (Proofterm.legacy_freezeT prop1, ZTerm.todo_proof) der, |
1962 fun zprf p = ZTerm.legacy_freezeT_proof prop1 p; |
|
1963 in |
|
1964 Thm (deriv_rule1 (prf, zprf) der, |
1963 {cert = cert, |
1965 {cert = cert, |
1964 tags = [], |
1966 tags = [], |
1965 maxidx = maxidx_of_term prop2, |
1967 maxidx = maxidx_of_term prop2, |
1966 constraints = constraints, |
1968 constraints = constraints, |
1967 shyps = shyps, |
1969 shyps = shyps, |