1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 08:44:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Feb 20 08:44:24 2013 +0100
     1.3 @@ -536,16 +536,19 @@
     1.4          add_step_pre ind qs subproofs
     1.5          #> add_suffix (of_prove qs (length subproofs) ^ " ")
     1.6          #> add_step_post ind l t facts ""
     1.7 -      | add_step ind (Obtain (qs, Fix xs, l, t,
     1.8 -                      By_Metis (subproofs, facts))) =
     1.9 +      | add_step ind (Obtain (qs, Fix xs, l, t, By_Metis (subproofs, facts))) =
    1.10          add_step_pre ind qs subproofs
    1.11          #> add_suffix (of_obtain qs (length subproofs) ^ " ")
    1.12          #> add_frees xs
    1.13          #> add_suffix " where "
    1.14          (* The new skolemizer puts the arguments in the same order as the ATPs
    1.15 -         (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
    1.16 -         Vampire). *)
    1.17 -        #> add_step_post ind l t facts "using [[metis_new_skolem]] "
    1.18 +           (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding
    1.19 +           Vampire). *)
    1.20 +        #> add_step_post ind l t facts
    1.21 +               (if exists (fn (_, T) => length (binder_types T) > 1) xs then
    1.22 +                  "using [[metis_new_skolem]] "
    1.23 +                else
    1.24 +                  "")
    1.25      and add_steps ind steps =
    1.26        fold (add_step ind) steps
    1.27      and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
    1.28 @@ -616,17 +619,13 @@
    1.29            val (l, subst, next) =
    1.30              (l, subst, next) |> fresh_label depth have_prefix
    1.31            val by = by |> do_byline subst depth
    1.32 -        in
    1.33 -          Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps
    1.34 -        end
    1.35 +        in Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end
    1.36        | do_steps subst depth next (Prove (qs, l, t, by) :: steps) =
    1.37          let
    1.38            val (l, subst, next) =
    1.39              (l, subst, next) |> fresh_label depth have_prefix
    1.40            val by = by |> do_byline subst depth
    1.41 -        in
    1.42 -          Prove (qs, l, t, by) :: do_steps subst depth next steps
    1.43 -        end
    1.44 +        in Prove (qs, l, t, by) :: do_steps subst depth next steps end
    1.45        | do_steps subst depth next (step :: steps) =
    1.46          step :: do_steps subst depth next steps
    1.47      and do_proof subst depth (Proof (fix, assms, steps)) =
    1.48 @@ -645,7 +644,7 @@
    1.49          if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0)
    1.50          else ([], lfs)
    1.51      fun chain_step lbl (Obtain (qs, xs, l, t,
    1.52 -                                        By_Metis (subproofs, (lfs, gfs)))) =
    1.53 +                                By_Metis (subproofs, (lfs, gfs)))) =
    1.54          let val (qs', lfs) = do_qs_lfs lbl lfs in
    1.55            Obtain (qs' @ qs, xs, l, t,
    1.56              By_Metis (chain_proofs subproofs, (lfs, gfs)))