generalized preplaying infrastructure to store various results for various methods
authorblanchet
Fri Jan 31 19:16:41 2014 +0100 (2014-01-31)
changeset 552233c593bad6b31
parent 55222 a4ef6eb1fc20
child 55226 46c8969a995b
generalized preplaying infrastructure to store various results for various methods
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 18:43:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jan 31 19:16:41 2014 +0100
     1.3 @@ -277,11 +277,15 @@
     1.4            |> postprocess_isar_proof_remove_unreferenced_steps I
     1.5            |> relabel_isar_proof_canonically
     1.6  
     1.7 -        val preplay_data as {string_of_preplay_outcome, overall_preplay_outcome, ...} =
     1.8 +        val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
     1.9            preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.10              preplay_timeout isar_proof
    1.11  
    1.12 -        fun str_of_meth l meth = string_of_proof_method meth ^ " " ^ string_of_preplay_outcome l
    1.13 +        fun str_of_preplay_outcome outcome =
    1.14 +          if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
    1.15 +
    1.16 +        fun str_of_meth l meth =
    1.17 +          string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
    1.18          fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
    1.19  
    1.20          fun trace_isar_proof label proof =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 18:43:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Jan 31 19:16:41 2014 +0100
     2.3 @@ -79,14 +79,15 @@
     2.4      | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
     2.5    end
     2.6  
     2.7 -(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
     2.8 +(* Tries merging the first step into the second step.
     2.9 +   FIXME: Arbitrarily picks the second step's method. *)
    2.10  fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
    2.11 -      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
    2.12 +      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
    2.13      let
    2.14        val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    2.15        val gfs = union (op =) gfs1 gfs2
    2.16      in
    2.17 -      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
    2.18 +      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
    2.19      end
    2.20    | try_merge _ _ = NONE
    2.21  
    2.22 @@ -136,57 +137,55 @@
    2.23  
    2.24        (** elimination of trivial, one-step subproofs **)
    2.25  
    2.26 -      fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
    2.27 +      fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
    2.28          if null subs orelse not (compress_further ()) then
    2.29 -          (set_preplay_outcome l (Played time);
    2.30 -           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
    2.31 +          (set_preplay_outcome l meth (Played time);
    2.32 +           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
    2.33          else
    2.34            (case subs of
    2.35              (sub as Proof (_, assms, sub_steps)) :: subs =>
    2.36              (let
    2.37 -              (* trivial subproofs have exactly one Prove step *)
    2.38 -              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
    2.39 +              (* trivial subproofs have exactly one "Prove" step *)
    2.40 +              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
    2.41 +                try the_single sub_steps
    2.42  
    2.43                (* only touch proofs that can be preplayed sucessfully *)
    2.44 -              val Played time' = preplay_outcome l'
    2.45 +              val Played time' = Lazy.force (preplay_outcome l' meth')
    2.46  
    2.47                (* merge steps *)
    2.48                val subs'' = subs @ nontriv_subs
    2.49 -              val lfs'' =
    2.50 -                subtract (op =) (map fst assms) lfs'
    2.51 -                |> union (op =) lfs
    2.52 +              val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
    2.53                val gfs'' = union (op =) gfs' gfs
    2.54 -              val by = ((lfs'', gfs''), meth)
    2.55 +              val by = ((lfs'', gfs''), methss(*FIXME*))
    2.56                val step'' = Prove (qs, fix, l, t, subs'', by)
    2.57  
    2.58                (* check if the modified step can be preplayed fast enough *)
    2.59                val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
    2.60                val Played time'' = preplay_quietly timeout step''
    2.61 -
    2.62              in
    2.63                decrement_step_count (); (* l' successfully eliminated! *)
    2.64                map (replace_successor l' [l]) lfs';
    2.65 -              elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
    2.66 +              elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
    2.67              end
    2.68              handle Bind =>
    2.69 -              elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
    2.70 +            elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
    2.71            | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
    2.72  
    2.73        fun elim_subproofs (step as Let _) = step
    2.74 -        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
    2.75 +        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
    2.76 +            ((lfs, gfs), methss as (meth :: _) :: _))) =
    2.77            if subproofs = [] then
    2.78              step
    2.79            else
    2.80 -            (case preplay_outcome l of
    2.81 -              Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
    2.82 +            (case Lazy.force (preplay_outcome l meth) of
    2.83 +              Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
    2.84              | _ => step)
    2.85  
    2.86        (** top_level compression: eliminate steps by merging them into their successors **)
    2.87 -
    2.88        fun compress_top_level steps =
    2.89          let
    2.90            (* (#successors, (size_of_term t, position)) *)
    2.91 -          fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
    2.92 +          fun cand_key (i, l, t_size) = (length (get_successors l), (t_size, i))
    2.93  
    2.94            val compression_ord =
    2.95              prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
    2.96 @@ -207,32 +206,36 @@
    2.97                  | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
    2.98              in
    2.99                (steps
   2.100 -              |> split_last |> fst (* keep last step *)
   2.101 -              |> fold_index add_cand) []
   2.102 +               |> split_last |> fst (* keep last step *)
   2.103 +               |> fold_index add_cand) []
   2.104              end
   2.105  
   2.106            fun try_eliminate (i, l, _) succ_lbls steps =
   2.107              let
   2.108 +              val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
   2.109 +                drop i steps
   2.110 +
   2.111 +              val succs = collect_successors steps' succ_lbls
   2.112 +              val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
   2.113 +
   2.114                (* only touch steps that can be preplayed successfully *)
   2.115 -              val Played time = preplay_outcome l
   2.116 +              val Played time = Lazy.force (preplay_outcome l meth)
   2.117  
   2.118 -              val succ_times = map (preplay_outcome #> (fn Played t => t)) succ_lbls
   2.119 +              val succs' = map (try_merge cand #> the) succs
   2.120 +
   2.121 +              val succ_times =
   2.122 +                map2 ((fn Played t => t) o Lazy.force oo preplay_outcome) succ_lbls succ_meths
   2.123                val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
   2.124                val timeouts =
   2.125                  map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
   2.126  
   2.127 -              val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
   2.128 -
   2.129                (* FIXME: debugging *)
   2.130                val _ =
   2.131 -                if the (label_of_step cand) <> l then
   2.132 +                if the (label_of_isar_step cand) <> l then
   2.133                    raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
   2.134                  else
   2.135                    ()
   2.136  
   2.137 -              val succs = collect_successors steps' succ_lbls
   2.138 -              val succs' = map (try_merge cand #> the) succs
   2.139 -
   2.140                (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
   2.141                val play_outcomes = map2 preplay_quietly timeouts succs'
   2.142  
   2.143 @@ -244,7 +247,7 @@
   2.144                val steps2 = update_steps steps2 succs'
   2.145              in
   2.146                decrement_step_count (); (* candidate successfully eliminated *)
   2.147 -              map2 set_preplay_outcome succ_lbls play_outcomes;
   2.148 +              map3 set_preplay_outcome succ_lbls succ_meths play_outcomes;
   2.149                map (replace_successor l succ_lbls) lfs;
   2.150                (* removing the step would mess up the indices -> replace with dummy step instead *)
   2.151                steps1 @ dummy_isar_step :: steps2
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 18:43:16 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Jan 31 19:16:41 2014 +0100
     3.3 @@ -27,11 +27,11 @@
     3.4  
     3.5  fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
     3.6    | minimize_isar_step_dependencies {preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
     3.7 -      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
     3.8 -    (case preplay_outcome l of
     3.9 +      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
    3.10 +    (case Lazy.force (preplay_outcome l meth) of
    3.11        Played time =>
    3.12        let
    3.13 -        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
    3.14 +        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
    3.15          val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
    3.16  
    3.17          fun minimize_facts _ time min_facts [] = (time, min_facts)
    3.18 @@ -43,7 +43,7 @@
    3.19          val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
    3.20          val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
    3.21        in
    3.22 -        set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
    3.23 +        set_preplay_outcome l meth (Played time); mk_step_lfs_gfs min_lfs min_gfs
    3.24        end
    3.25      | _ => step (* don't touch steps that time out or fail *))
    3.26  
    3.27 @@ -62,7 +62,7 @@
    3.28            fold_rev do_step steps (refed, [concl])
    3.29          end
    3.30      and do_step step (refed, accu) =
    3.31 -      (case label_of_step step of
    3.32 +      (case label_of_isar_step step of
    3.33          NONE => (refed, step :: accu)
    3.34        | SOME l =>
    3.35          if Ord_List.member label_ord refed l then
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 18:43:16 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Fri Jan 31 19:16:41 2014 +0100
     4.3 @@ -8,6 +8,7 @@
     4.4  signature SLEDGEHAMMER_ISAR_PREPLAY =
     4.5  sig
     4.6    type play_outcome = Sledgehammer_Reconstructor.play_outcome
     4.7 +  type proof_method = Sledgehammer_Isar_Proof.proof_method
     4.8    type isar_step = Sledgehammer_Isar_Proof.isar_step
     4.9    type isar_proof = Sledgehammer_Isar_Proof.isar_proof
    4.10    type label = Sledgehammer_Isar_Proof.label
    4.11 @@ -15,9 +16,8 @@
    4.12    val trace : bool Config.T
    4.13  
    4.14    type isar_preplay_data =
    4.15 -    {preplay_outcome: label -> play_outcome,
    4.16 -     set_preplay_outcome: label -> play_outcome -> unit,
    4.17 -     string_of_preplay_outcome: label -> string,
    4.18 +    {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    4.19 +     set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    4.20       preplay_quietly: Time.time -> isar_step -> play_outcome,
    4.21       overall_preplay_outcome: isar_proof -> play_outcome}
    4.22  
    4.23 @@ -106,9 +106,8 @@
    4.24      | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
    4.25  
    4.26  (* main function for preplaying Isar steps; may throw exceptions *)
    4.27 -fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
    4.28 -  | preplay_raw debug type_enc lam_trans ctxt timeout
    4.29 -      (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
    4.30 +fun preplay_raw debug type_enc lam_trans ctxt timeout meth
    4.31 +      (Prove (_, xs, _, t, subproofs, (fact_names, _))) =
    4.32      let
    4.33        val goal =
    4.34          (case xs of
    4.35 @@ -147,9 +146,8 @@
    4.36      end
    4.37  
    4.38  type isar_preplay_data =
    4.39 -  {preplay_outcome: label -> play_outcome,
    4.40 -   set_preplay_outcome: label -> play_outcome -> unit,
    4.41 -   string_of_preplay_outcome: label -> string,
    4.42 +  {preplay_outcome: label -> proof_method -> play_outcome Lazy.lazy,
    4.43 +   set_preplay_outcome: label -> proof_method -> play_outcome -> unit,
    4.44     preplay_quietly: Time.time -> isar_step -> play_outcome,
    4.45     overall_preplay_outcome: isar_proof -> play_outcome}
    4.46  
    4.47 @@ -188,17 +186,16 @@
    4.48  fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    4.49    if not do_preplay then
    4.50      (* the "dont_preplay" option pretends that everything works just fine *)
    4.51 -    {preplay_outcome = K (Played Time.zeroTime),
    4.52 -     set_preplay_outcome = K (K ()),
    4.53 -     string_of_preplay_outcome = K "",
    4.54 +    {preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
    4.55 +     set_preplay_outcome = K (K (K ())),
    4.56       preplay_quietly = K (K (Played Time.zeroTime)),
    4.57       overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    4.58    else
    4.59      let
    4.60        val ctxt = enrich_context_with_local_facts proof ctxt
    4.61  
    4.62 -      fun preplay quietly timeout step =
    4.63 -        preplay_raw debug type_enc lam_trans ctxt timeout step
    4.64 +      fun preplay quietly timeout meth step =
    4.65 +        preplay_raw debug type_enc lam_trans ctxt timeout meth step
    4.66          handle exn =>
    4.67            if Exn.is_interrupt exn then
    4.68              reraise exn
    4.69 @@ -210,43 +207,42 @@
    4.70               Play_Failed)
    4.71  
    4.72        (* preplay steps treating exceptions like timeouts *)
    4.73 -      fun preplay_quietly timeout = preplay true timeout
    4.74 +      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
    4.75 +          preplay true timeout meth step
    4.76 +        | preplay_quietly _ _ = Played Time.zeroTime
    4.77 +
    4.78 +      fun add_step_to_tab (step as Prove (_, _, l, _, _, (_, methss))) =
    4.79 +          Canonical_Label_Tab.update_new
    4.80 +            (l, maps (map (fn meth =>
    4.81 +               (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
    4.82 +        | add_step_to_tab _ = I
    4.83  
    4.84        val preplay_tab =
    4.85 -        let
    4.86 -          fun add_step_to_tab step tab =
    4.87 -            (case label_of_step step of
    4.88 -              NONE => tab
    4.89 -            | SOME l =>
    4.90 -              Canonical_Label_Tab.update_new
    4.91 -                (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
    4.92 -            handle Canonical_Label_Tab.DUP _ =>
    4.93 -              raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
    4.94 -        in
    4.95 -          Canonical_Label_Tab.empty
    4.96 -          |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
    4.97 -          |> Unsynchronized.ref
    4.98 -        end
    4.99 +        Canonical_Label_Tab.empty
   4.100 +        |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
   4.101 +        |> Unsynchronized.ref
   4.102  
   4.103 -      fun preplay_outcome l =
   4.104 -        Canonical_Label_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
   4.105 -        handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
   4.106 +      fun preplay_outcome l meth =
   4.107 +        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
   4.108 +          SOME meths_outcomes =>
   4.109 +          (case AList.lookup (op =) meths_outcomes meth of
   4.110 +            SOME outcome => outcome
   4.111 +          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
   4.112 +        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
   4.113  
   4.114 -      fun set_preplay_outcome l result =
   4.115 -        preplay_tab := Canonical_Label_Tab.update (l, Lazy.value result) (!preplay_tab)
   4.116 +      fun set_preplay_outcome l meth result =
   4.117 +        preplay_tab := Canonical_Label_Tab.map_entry l
   4.118 +          (AList.update (op =) (meth, Lazy.value result)) (!preplay_tab)
   4.119  
   4.120 -      fun string_of_preplay_outcome l = @{make_string} (preplay_outcome l)
   4.121 -
   4.122 -      val result_of_step =
   4.123 -        try (label_of_step #> the #> preplay_outcome)
   4.124 -        #> the_default (Played Time.zeroTime)
   4.125 +      fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
   4.126 +          Lazy.force (preplay_outcome l meth)
   4.127 +        | result_of_step _ = Played Time.zeroTime
   4.128  
   4.129        fun overall_preplay_outcome (Proof (_, _, steps)) =
   4.130          fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
   4.131      in
   4.132        {preplay_outcome = preplay_outcome,
   4.133         set_preplay_outcome = set_preplay_outcome,
   4.134 -       string_of_preplay_outcome = string_of_preplay_outcome,
   4.135         preplay_quietly = preplay_quietly,
   4.136         overall_preplay_outcome = overall_preplay_outcome}
   4.137      end
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 18:43:16 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Fri Jan 31 19:16:41 2014 +0100
     5.3 @@ -34,8 +34,8 @@
     5.4  
     5.5    val steps_of_proof : isar_proof -> isar_step list
     5.6  
     5.7 -  val label_of_step : isar_step -> label option
     5.8 -  val byline_of_step : isar_step -> (facts * proof_method list list) option
     5.9 +  val label_of_isar_step : isar_step -> label option
    5.10 +  val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
    5.11  
    5.12    val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    5.13    val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    5.14 @@ -103,17 +103,17 @@
    5.15  
    5.16  fun steps_of_proof (Proof (_, _, steps)) = steps
    5.17  
    5.18 -fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
    5.19 -  | label_of_step _ = NONE
    5.20 +fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
    5.21 +  | label_of_isar_step _ = NONE
    5.22  
    5.23 -fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
    5.24 -  | subproofs_of_step _ = NONE
    5.25 +fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
    5.26 +  | subproofs_of_isar_step _ = NONE
    5.27  
    5.28 -fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
    5.29 -  | byline_of_step _ = NONE
    5.30 +fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = SOME byline
    5.31 +  | byline_of_isar_step _ = NONE
    5.32  
    5.33  fun fold_isar_step f step =
    5.34 -  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
    5.35 +  fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
    5.36  and fold_isar_steps f = fold (fold_isar_step f)
    5.37  
    5.38  fun map_isar_steps f =
    5.39 @@ -143,15 +143,15 @@
    5.40    | chain_isar_step _ step = step
    5.41  and chain_isar_steps _ [] = []
    5.42    | chain_isar_steps (prev as SOME _) (i :: is) =
    5.43 -    chain_isar_step prev i :: chain_isar_steps (label_of_step i) is
    5.44 -  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_step i) is
    5.45 +    chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
    5.46 +  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
    5.47  and chain_isar_proof (Proof (fix, assms, steps)) =
    5.48    Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
    5.49  
    5.50  fun kill_useless_labels_in_isar_proof proof =
    5.51    let
    5.52      val used_ls =
    5.53 -      fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
    5.54 +      fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
    5.55          (steps_of_proof proof) []
    5.56  
    5.57      fun kill_label l = if member (op =) used_ls l then l else no_label
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 18:43:16 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Fri Jan 31 19:16:41 2014 +0100
     6.3 @@ -31,10 +31,10 @@
     6.4  fun try0_step _ _ (step as Let _) = step
     6.5    | try0_step preplay_timeout
     6.6        ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
     6.7 -      (step as Prove (_, _, l, _, _, _)) =
     6.8 +      (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
     6.9      let
    6.10        val timeout =
    6.11 -        (case preplay_outcome l of
    6.12 +        (case Lazy.force (preplay_outcome l meth) of
    6.13            Played time => Time.+ (time, slack)
    6.14          | _ => preplay_timeout)
    6.15  
    6.16 @@ -44,7 +44,8 @@
    6.17          | _ => NONE)
    6.18      in
    6.19        (case Par_List.get_some try_variant (variants_of_step step) of
    6.20 -        SOME (step', result) => (set_preplay_outcome l result; step')
    6.21 +        SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
    6.22 +        (set_preplay_outcome l meth' result; step')
    6.23        | NONE => step)
    6.24      end
    6.25  
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 18:43:16 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jan 31 19:16:41 2014 +0100
     7.3 @@ -8,6 +8,7 @@
     7.4  sig
     7.5    val sledgehammerN : string
     7.6    val log2 : real -> real
     7.7 +  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
     7.8    val app_hd : ('a -> 'a) -> 'a list -> 'a list
     7.9    val n_fold_cartesian_product : 'a list list -> 'a list list
    7.10    val plural_s : int -> string
    7.11 @@ -38,6 +39,8 @@
    7.12  val log10_2 = Math.log10 2.0
    7.13  fun log2 n = Math.log10 n / log10_2
    7.14  
    7.15 +fun map3 xs = Ctr_Sugar_Util.map3 xs
    7.16 +
    7.17  fun app_hd f (x :: xs) = f x :: xs
    7.18  
    7.19  fun cartesian_product [] _ = []