1375 in |
1375 in |
1376 (case (prop1, prop2) of |
1376 (case (prop1, prop2) of |
1377 (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, |
1377 (Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g, |
1378 Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => |
1378 Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) => |
1379 (chktypes fT tT; |
1379 (chktypes fT tT; |
1380 Thm (deriv_rule2 (Proofterm.combination_proof (domain_type fT) f g t u) der1 der2, |
1380 Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2, |
1381 {cert = join_certificate2 (th1, th2), |
1381 {cert = join_certificate2 (th1, th2), |
1382 tags = [], |
1382 tags = [], |
1383 maxidx = Int.max (maxidx1, maxidx2), |
1383 maxidx = Int.max (maxidx1, maxidx2), |
1384 constraints = union_constraints constraints1 constraints2, |
1384 constraints = union_constraints constraints1 constraints2, |
1385 shyps = Sorts.union shyps1 shyps2, |
1385 shyps = Sorts.union shyps1 shyps2, |