# HG changeset patch
# User blanchet
# Date 1327940159 -3600
# Node ID 723343a03abeae770766c7e5bd07e219d23a2ef2
# Parent  2ded91a6cbd5c287405fc46e47f1e1600502d733
avoid unsupported case in Metis

diff -r 2ded91a6cbd5 -r 723343a03abe src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Jan 30 17:15:59 2012 +0100
@@ -179,8 +179,8 @@
         is_axiom_used_in_proof is_lam_lifted atp_proof) of
     (false, false) => default
   | (false, true) => liftingN
-  | (true, false) => combsN
-  | (true, true) => combs_and_liftingN
+(*  | (true, true) => combs_and_liftingN -- not supported by "metis" *)
+  | (true, _) => combsN
 
 val is_typed_helper_name =
   String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix