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_try0.ML
changeset 55243 66709d41601e
parent 55223 3c593bad6b31
child 55244 12e1a5d8ee48 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 19:15:25 2014 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -43,6 +43,7 @@
           result as Played _ => SOME (variant, result)
         | _ => NONE)
     in
+      (* FIXME: create variant after success *)
       (case Par_List.get_some try_variant (variants_of_step step) of
         SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
         (set_preplay_outcome l meth' result; step')
isabelle