# HG changeset patch
# User blanchet
# Date 1394713093 -3600
# Node ID 75c154e9f65064ed53d1c533f25fee96f7d2d910
# Parent  b5d1d9c60341b80269df0a4cbacb065d484e6b03
honor the fact that the new Z3 can generate Isar proofs

diff -r b5d1d9c60341 -r 75c154e9f650 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Mar 13 13:18:13 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Mar 13 13:18:13 2014 +0100
@@ -247,9 +247,10 @@
   end
 
 val canonical_isar_supported_prover = eN
+val z3_newN = "z3_new"
 
 fun isar_supported_prover_of thy name =
-  if is_atp thy name then name
+  if is_atp thy name orelse name = z3_newN then name
   else if is_atp_installed thy canonical_isar_supported_prover then canonical_isar_supported_prover
   else name
 
@@ -260,7 +261,7 @@
     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
     val (min_name, override_params) =
       (case preplay of
-        (meth, Played _) =>
+        (meth as Metis_Method _, Played _) =>
         if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
       | _ => (maybe_isar_name, []))
   in minimize_command override_params min_name end