equal
deleted
inserted
replaced
1266 let |
1266 let |
1267 val prop1 = attach_tpairs tpairs prop; |
1267 val prop1 = attach_tpairs tpairs prop; |
1268 val prop2 = Type.legacy_freeze prop1; |
1268 val prop2 = Type.legacy_freeze prop1; |
1269 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1269 val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2); |
1270 in |
1270 in |
1271 Thm (deriv_rule1 (Pt.freezeT prop1) der, |
1271 Thm (deriv_rule1 (Pt.legacy_freezeT prop1) der, |
1272 {thy_ref = thy_ref, |
1272 {thy_ref = thy_ref, |
1273 tags = [], |
1273 tags = [], |
1274 maxidx = maxidx_of_term prop2, |
1274 maxidx = maxidx_of_term prop2, |
1275 shyps = shyps, |
1275 shyps = shyps, |
1276 hyps = hyps, |
1276 hyps = hyps, |