# HG changeset patch
# User blanchet
# Date 1410784292 -7200
# Node ID 9a82544fd29f3788a962412aac9455c523a9b052
# Parent  6c8b30b9f58310dc9b23e0c8b38bc68c7011b43d
tuning

diff -r 6c8b30b9f583 -r 9a82544fd29f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 15 12:30:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 15 14:31:32 2014 +0200
@@ -278,12 +278,12 @@
                 (case gamma of
                   [g] =>
                   if skolem andalso is_clause_tainted g then
-                    (case skolems_of ctxt (prop_of_clause g) of
-                      [] => steps_of_rest (prove [] deps)
-                    | skos =>
-                      let val subproof = Proof (skos, [], rev accum) in
-                        isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
-                      end)
+                    let
+                      val skos = skolems_of ctxt (prop_of_clause g)
+                      val subproof = Proof (skos, [], rev accum)
+                    in
+                      isar_steps outer (SOME l) [prove [subproof] ([], [])] infs
+                    end
                   else
                     steps_of_rest (prove [] deps)
                 | _ => steps_of_rest (prove [] deps))
@@ -317,9 +317,9 @@
 
         val canonical_isar_proof =
           refute_graph
-          |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
+          |> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph)
           |> redirect_graph axioms tainted bot
-          |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
+          |> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof)
           |> isar_proof true params assms lems
           |> postprocess_isar_proof_remove_show_stuttering
           |> postprocess_isar_proof_remove_unreferenced_steps I