# HG changeset patch
# User blanchet
# Date 1297268338 -3600
# Node ID d52af5722f0f1686d619ba024d41f7d04f4189ec
# Parent  11e862c68b40e8fd2eca504e1c0523f6a2501451
tuning

diff -r 11e862c68b40 -r d52af5722f0f src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -113,22 +113,32 @@
     fun split [] p = p
       | split [h] (l, r) = (h :: l, r)
       | split (h1 :: h2 :: t) (l, r) = split t (h1 :: l, h2 :: r)
-    fun min _ [] = raise Empty
-      | min _ [s0] = [s0]
-      | min sup xs =
-        let val (l0, r0) = split xs ([], []) in
+    fun min _ _ [] = raise Empty
+      | min _ _ [s0] = [s0]
+      | min depth sup xs =
+        let
+(*
+          val _ = warning (replicate_string depth " " ^ "{" ^ ("  " ^
+                           n_facts (map fst sup) ^ " and " ^
+                           n_facts (map fst xs)))
+*)
+          val (l0, r0) = split xs ([], [])
+        in
           if p (sup @ l0) then
-            min sup l0
+            min (depth + 1) sup l0
           else if p (sup @ r0) then
-            min sup r0
+            min (depth + 1) sup r0
           else
             let
-              val l = min (sup @ r0) l0
-              val r = min (sup @ l) r0
+              val l = min (depth + 1) (sup @ r0) l0
+              val r = min (depth + 1) (sup @ l) r0
             in l @ r end
         end
+(*
+        |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
+*)
     val xs =
-      case min [] xs of
+      case min 0 [] xs of
         [x] => if p [] then [] else [x]
       | xs => xs
   in (xs, test xs) end
diff -r 11e862c68b40 -r d52af5722f0f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Feb 09 17:18:58 2011 +0100
@@ -36,11 +36,11 @@
      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    else
      "") ^
-  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^ ":" ^
+  " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
   (if blocking then
-     ""
+     "."
    else
-     "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
+     ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
 
 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)