# HG changeset patch
# User wenzelm
# Date 1571237241 -7200
# Node ID 9ff9559f1ee203704cfe9ff4ce420e7ee1c8f7d6
# Parent  de6f137a07d3d03d599c236c914cb7c0aa80540c
more informative combination_proof, e.g. relevant for proper type inference in HOL.Product_Type (with export_proofs);

diff -r de6f137a07d3 -r 9ff9559f1ee2 src/Pure/proofterm.ML
--- 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;