Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
changeset 55295 b18f65f77fcd
parent 55294 6f77310a0907
child 55299 c3bb1cffce26 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -208,7 +208,7 @@
   #> fst
 
 fun forced_outcome_of_step preplay_data (Prove (_, _, l, _, _, _, meths)) =
-    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (the_single meths))
+    Lazy.force (preplay_outcome_of_isar_step_for_method preplay_data l (hd meths))
   | forced_outcome_of_step _ _ = Played Time.zeroTime
 
 fun preplay_outcome_of_isar_proof preplay_data (Proof (_, _, steps)) =
isabelle