# HG changeset patch
# User wenzelm
# Date 1571491952 -7200
# Node ID 3828a57e537d5578a651d65b90075aab0cf5d273
# Parent  7e3f25a0cee492fc5614b7a43a2d0aeb30c9e6e1
tuned signature;

diff -r 7e3f25a0cee4 -r 3828a57e537d src/Pure/proofterm.ML
--- 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;
diff -r 7e3f25a0cee4 -r 3828a57e537d src/Pure/thm.ML
--- 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),