# HG changeset patch
# User nipkow
# Date 1253348374 -7200
# Node ID 0bc4f7e3e2d3e32f165058084569666e034b9559
# Parent  210fa627d7677eea6faf28451f9d42344795e673# Parent  76dddd260d2f3d1bd0d34760f78460ff9bb02d11
merged

diff -r 210fa627d767 -r 0bc4f7e3e2d3 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 19 07:35:27 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 19 10:19:34 2009 +0200
@@ -410,20 +410,20 @@
     val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
         inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
     val named_thms = ref (NONE : (string * thm list) list option)
-
-    fun if_enabled k f =
-      if AList.defined (op =) args k andalso is_some (!named_thms)
-      then f id st else ()
-
-    val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
-    val _ = if_enabled minimizeK
-      (Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))))
-    val _ = if_enabled minimizeK
-      (Mirabelle.catch minimize_tag (run_minimize args named_thms))
-    val _ = if is_some (!named_thms)
-      then Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st
-      else ()
-  in () end
+    val minimize = AList.defined (op =) args minimizeK
+  in 
+    Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
+    if is_some (!named_thms)
+      then
+       (if minimize
+          then Mirabelle.catch metis_tag (run_metis metis0_fns args (these (!named_thms))) id st
+          else ();
+       if minimize andalso not(null(these(!named_thms)))
+         then Mirabelle.catch minimize_tag (run_minimize args named_thms) id st
+         else ();
+       Mirabelle.catch metis_tag (run_metis metis_fns args (these (!named_thms))) id st)
+    else ()
+  end
 
 fun invoke args =
   let