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 55279 df41d34d1324
parent 55278 73372494fd80
child 55280 f0187a12b8f2 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -169,7 +169,7 @@
         outcome as Played _ => SOME (meth, outcome)
       | _ => NONE)
 
-    val meths = snd (byline_of_isar_step step)
+    val meths = proof_methods_of_isar_step step
   in
     the_list (Par_List.get_some try_method meths)
   end
isabelle