# HG changeset patch
# User nipkow
# Date 1253277624 -7200
# Node ID c0056c2c1d17dff5c2231537ca51d25399e8f168
# Parent  b5c3a8a7577245b91aa805e57c327fef1ed93088# Parent  e7fe01b74a9200f24f65c31771c1b19cb25e48d7
merged

diff -r b5c3a8a75772 -r c0056c2c1d17 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 18 14:09:38 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 18 14:40:24 2009 +0200
@@ -396,7 +396,9 @@
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
+fun sledgehammer_action args id (st as {log, pre, ...}: Mirabelle.run_args) =
+  if can Logic.dest_conjunction (Thm.major_prem_of(snd(snd(Proof.get_goal pre))))
+  then () else
   let
     val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
         inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)