more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);

--- a/src/Pure/proofterm.ML	Wed Oct 16 15:31:01 2019 +0200
+++ b/src/Pure/proofterm.ML	Wed Oct 16 16:47:21 2019 +0200
@@ -1326,17 +1326,15 @@
             combination_axm %> remove_types f % NONE
         | _ => combination_axm %> remove_types f %> remove_types g)
   in
-    (case A of
-      Type ("fun", _) => prf %
-        (case head_of f of
-          Abs _ => SOME (remove_types t)
-        | Var _ => SOME (remove_types t)
-        | _ => NONE) %
-        (case head_of g of
-          Abs _ => SOME (remove_types u)
-        | Var _ => SOME (remove_types u)
-        | _ => NONE) %% prf1 %% prf2
-     | _ => prf % NONE % NONE %% prf1 %% prf2)
+    prf %
+      (case head_of f of
+        Abs _ => SOME (remove_types t)
+      | Var _ => SOME (remove_types t)
+      | _ => NONE) %
+      (case head_of g of
+        Abs _ => SOME (remove_types u)
+      | Var _ => SOME (remove_types u)
+      | _ => NONE) %% prf1 %% prf2
   end;