--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 04 00:04:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Tue Feb 04 01:03:28 2014 +0100
@@ -146,10 +146,8 @@
(case preplay_isar_step_for_method ctxt timeout meth step of
outcome as Played _ => SOME (meth, outcome)
| _ => NONE)
-
- val meths = proof_methods_of_isar_step step
in
- the_list (Par_List.get_some try_method meths)
+ the_list (Par_List.get_some try_method (proof_methods_of_isar_step step))
end
type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table