src/Pure/proofterm.ML

   val symmetric_proof: proof -> proof
   val transitive_proof: typ -> term -> proof -> proof -> proof
   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 ->
     (class * class -> proof) ->
     (string * class list list * class -> proof) ->

   | check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
       check_comb prf1 andalso check_comb prf2
   | 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;
     val prf =
       if check_comb prf1 then