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