--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 18:39:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 19:16:44 2013 +0100
@@ -1027,9 +1027,8 @@
raise Fail ("unknown reconstructor: " ^ quote name)
val used_facts = facts |> map fst
in
- (case play_one_line_proof (if mode = Minimize then Normal else mode) debug
- verbose timeout facts state subgoal reconstr
- [reconstr] of
+ (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
+ state subgoal reconstr [reconstr] of
play as (_, Played time) =>
{outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
preplay = Lazy.value play,