Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authornipkow
Fri, 18 Sep 2009 14:40:24 +0200
changeset 32608 c0056c2c1d17
parent 32606 b5c3a8a75772 (current diff)
parent 32607 e7fe01b74a92 (diff)
child 32609 2f3e7a92b522
child 32610 c477b0a62ce9
child 32618 42865636d006
merged
--- 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)
isabelle