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:56:34 2013 +0100
     1.3 @@ -549,8 +549,7 @@
     1.4                    "using [[metis_new_skolem]] "
     1.5                  else
     1.6                    "")
     1.7 -    and add_steps ind steps =
     1.8 -      fold (add_step ind) steps
     1.9 +    and add_steps ind = fold (add_step ind)
    1.10      and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) =
    1.11        ("", ctxt)
    1.12        |> add_fix ind xs
    1.13 @@ -568,12 +567,11 @@
    1.14    end
    1.15  
    1.16  fun add_labels_of_step step =
    1.17 -  (case byline_of_step step of
    1.18 -     NONE => I
    1.19 -  |  SOME (By_Metis (subproofs, (ls, _))) =>
    1.20 -      union (op =) (add_labels_of_proofs subproofs ls))
    1.21 +  case byline_of_step step of
    1.22 +    NONE => I
    1.23 +  | SOME (By_Metis (subproofs, (ls, _))) =>
    1.24 +    union (op =) ls #> fold add_labels_of_proof subproofs
    1.25  and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof)
    1.26 -and add_labels_of_proofs proofs = fold add_labels_of_proof proofs
    1.27  
    1.28  fun kill_useless_labels_in_proof proof =
    1.29    let