1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 19 15:21:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 19 15:24:57 2010 +0200
     1.3 @@ -517,20 +517,20 @@
     1.4      val lines = split_lines proof_extract
     1.5    in map_filter (inputno o toks) lines end
     1.6    
     1.7 -(*extracting lemmas from tstp-output between the lines from above*)
     1.8 -fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) =
     1.9 +(* Extracting lemmas from TSTP output between the lines from above. *)
    1.10 +fun extract_lemmas get_step_nums (proof, thm_names, conjecture_pos, _, _, _) =
    1.11    let
    1.12      (* get the names of axioms from their numbers*)
    1.13      fun get_axiom_names thm_names step_nums =
    1.14        let
    1.15          val last_axiom = Vector.length thm_names
    1.16          fun is_axiom n = n <= last_axiom
    1.17 -        fun is_conj n = n >= fst conj_count andalso
    1.18 -                        n < fst conj_count + snd conj_count
    1.19 -        fun getname i = Vector.sub(thm_names, i-1)
    1.20 +        fun is_conj n = n >= fst conjecture_pos andalso
    1.21 +                        n < fst conjecture_pos + snd conjecture_pos
    1.22 +        fun name_at i = Vector.sub (thm_names, i - 1)
    1.23        in
    1.24          (sort_distinct string_ord (filter (fn x => x <> "??.unknown")
    1.25 -          (map getname (filter is_axiom step_nums))),
    1.26 +          (map name_at (filter is_axiom step_nums))),
    1.27          exists is_conj step_nums)
    1.28        end
    1.29    in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end;
    1.30 @@ -574,7 +574,7 @@
    1.31    end
    1.32  
    1.33  fun isar_proof_text minimal modulus sorts atp_name
    1.34 -        (result as (proof, thm_names, conj_count, ctxt, goal, i)) =
    1.35 +                    (result as (proof, thm_names, _, ctxt, goal, i)) =
    1.36    let
    1.37      (* We could use "split_lines", but it can return blank lines. *)
    1.38      val lines = String.tokens (equal #"\n");