# 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