--- a/src/Pure/proofterm.ML Sat Oct 19 11:33:36 2019 +0200
+++ b/src/Pure/proofterm.ML Sat Oct 19 15:32:32 2019 +0200
@@ -136,7 +136,7 @@
val equal_intr_proof: term -> term -> proof -> proof -> proof
val equal_elim_proof: term -> term -> proof -> proof -> proof
val abstract_rule_proof: string * term -> proof -> proof
- val combination_proof: typ -> term -> term -> term -> term -> proof -> proof -> proof
+ val combination_proof: term -> term -> term -> term -> proof -> proof -> proof
val strip_shyps_proof: Sorts.algebra -> (typ * sort) list -> (typ * sort) list ->
sort list -> proof -> proof
val of_sort_proof: Sorts.algebra ->
@@ -1313,7 +1313,7 @@
| check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
| check_comb _ = false;
-fun combination_proof A f g t u prf1 prf2 =
+fun combination_proof f g t u prf1 prf2 =
let
val f = Envir.beta_norm f;
val g = Envir.beta_norm g;
--- a/src/Pure/thm.ML Sat Oct 19 11:33:36 2019 +0200
+++ b/src/Pure/thm.ML Sat Oct 19 15:32:32 2019 +0200
@@ -1377,7 +1377,7 @@
(Const ("Pure.eq", Type ("fun", [fT, _])) $ f $ g,
Const ("Pure.eq", Type ("fun", [tT, _])) $ t $ u) =>
(chktypes fT tT;
- Thm (deriv_rule2 (Proofterm.combination_proof (domain_type fT) f g t u) der1 der2,
+ Thm (deriv_rule2 (Proofterm.combination_proof f g t u) der1 der2,
{cert = join_certificate2 (th1, th2),
tags = [],
maxidx = Int.max (maxidx1, maxidx2),