--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 14:49:18 2013 +0100
@@ -21,8 +21,8 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, _ :: meths))) =
- map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) meths
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
+ map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
| variants_of_step _ = raise Fail "Sledgehammer_Try0: variants_of_step"
val slack = seconds 0.05