# HG changeset patch
# User nipkow
# Date 1253277606 -7200
# Node ID e7fe01b74a9200f24f65c31771c1b19cb25e48d7
# Parent  979c274089a504c09ab42e3afa03000721c2c641
skip &&& goals

diff -r 979c274089a5 -r e7fe01b74a92 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 19:13:22 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Sep 18 14:40:06 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)