1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 15:54:38 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 16:02:33 2013 +0100
     1.3 @@ -702,12 +702,11 @@
     1.4          fun maybe_show outer c =
     1.5            (outer andalso length c = 1 andalso subset (op =) (c, conjs))
     1.6            ? cons Show
     1.7 -        fun do_have outer qs (gamma, c) =
     1.8 -          Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,
     1.9 -                 By_Metis (fold (add_fact_from_dependencies fact_names) gamma
    1.10 -                                ([], [])))
    1.11 -        fun do_inf outer (Have z) = do_have outer [] z
    1.12 -          | do_inf outer (Cases cases) =
    1.13 +        fun isar_step_of_direct_inf outer (Have (gamma, c)) =
    1.14 +            Prove (maybe_show outer c [], label_of_clause c, prop_of_clause c,
    1.15 +                   By_Metis (fold (add_fact_from_dependencies fact_names) gamma
    1.16 +                                  ([], [])))
    1.17 +          | isar_step_of_direct_inf outer (Cases cases) =
    1.18              let val c = succedent_of_cases cases in
    1.19                Prove (maybe_show outer c [Ultimately], label_of_clause c,
    1.20                       prop_of_clause c,
    1.21 @@ -715,11 +714,11 @@
    1.22              end
    1.23          and do_case outer (c, infs) =
    1.24            Assume (label_of_clause c, prop_of_clause c) ::
    1.25 -          map (do_inf outer) infs
    1.26 +          map (isar_step_of_direct_inf outer) infs
    1.27          val (isar_proof, (preplay_fail, ext_time)) =
    1.28            ref_graph
    1.29            |> redirect_graph axioms tainted
    1.30 -          |> map (do_inf true)
    1.31 +          |> map (isar_step_of_direct_inf true)
    1.32            |> append assms
    1.33            |> (if not preplay andalso isar_shrink <= 1.0 then
    1.34                  pair (false, (true, seconds 0.0)) #> swap