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 18:43:16 2014 +0100
     1.3 @@ -103,89 +103,6 @@
     1.4          add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
     1.5      end
     1.6  
     1.7 -val add_labels_of_proof =
     1.8 -  steps_of_proof
     1.9 -  #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
    1.10 -
    1.11 -fun kill_useless_labels_in_proof proof =
    1.12 -  let
    1.13 -    val used_ls = add_labels_of_proof proof []
    1.14 -
    1.15 -    fun kill_label l = if member (op =) used_ls l then l else no_label
    1.16 -    fun kill_assms assms = map (apfst kill_label) assms
    1.17 -
    1.18 -    fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
    1.19 -        Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
    1.20 -      | kill_step step = step
    1.21 -    and kill_proof (Proof (fix, assms, steps)) =
    1.22 -      Proof (fix, kill_assms assms, map kill_step steps)
    1.23 -  in
    1.24 -    kill_proof proof
    1.25 -  end
    1.26 -
    1.27 -val assume_prefix = "a"
    1.28 -val have_prefix = "f"
    1.29 -
    1.30 -val relabel_proof =
    1.31 -  let
    1.32 -    fun fresh_label depth prefix (accum as (l, subst, next)) =
    1.33 -      if l = no_label then
    1.34 -        accum
    1.35 -      else
    1.36 -        let val l' = (replicate_string (depth + 1) prefix, next) in
    1.37 -          (l', (l, l') :: subst, next + 1)
    1.38 -        end
    1.39 -
    1.40 -    fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
    1.41 -
    1.42 -    fun relabel_assm depth (l, t) (subst, next) =
    1.43 -      let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
    1.44 -        ((l, t), (subst, next))
    1.45 -      end
    1.46 -
    1.47 -    fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
    1.48 -
    1.49 -    fun relabel_steps _ _ _ [] = []
    1.50 -      | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
    1.51 -        let
    1.52 -          val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
    1.53 -          val sub = relabel_proofs subst depth sub
    1.54 -          val by = apfst (relabel_facts subst) by
    1.55 -        in
    1.56 -          Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
    1.57 -        end
    1.58 -      | relabel_steps subst depth next (step :: steps) =
    1.59 -        step :: relabel_steps subst depth next steps
    1.60 -    and relabel_proof subst depth (Proof (fix, assms, steps)) =
    1.61 -      let val (assms, subst) = relabel_assms subst depth assms in
    1.62 -        Proof (fix, assms, relabel_steps subst depth 1 steps)
    1.63 -      end
    1.64 -    and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
    1.65 -  in
    1.66 -    relabel_proof [] 0
    1.67 -  end
    1.68 -
    1.69 -val chain_direct_proof =
    1.70 -  let
    1.71 -    fun chain_qs_lfs NONE lfs = ([], lfs)
    1.72 -      | chain_qs_lfs (SOME l0) lfs =
    1.73 -        if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
    1.74 -    fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
    1.75 -        let val (qs', lfs) = chain_qs_lfs lbl lfs in
    1.76 -          Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
    1.77 -        end
    1.78 -      | chain_step _ step = step
    1.79 -    and chain_steps _ [] = []
    1.80 -      | chain_steps (prev as SOME _) (i :: is) =
    1.81 -        chain_step prev i :: chain_steps (label_of_step i) is
    1.82 -      | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
    1.83 -    and chain_proof (Proof (fix, assms, steps)) =
    1.84 -      Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
    1.85 -    and chain_proofs proofs = map (chain_proof) proofs
    1.86 -  in
    1.87 -    chain_proof
    1.88 -  end
    1.89 -
    1.90  type isar_params =
    1.91    bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
    1.92  
    1.93 @@ -378,7 +295,9 @@
    1.94                 (try0_isar ? minimize_isar_step_dependencies preplay_data)
    1.95            |> tap (trace_isar_proof "Minimized")
    1.96            |> `overall_preplay_outcome
    1.97 -          ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
    1.98 +          ||> chain_isar_proof
    1.99 +          ||> kill_useless_labels_in_isar_proof
   1.100 +          ||> relabel_isar_proof_finally
   1.101        in
   1.102          (case string_of_isar_proof false isar_proof of
   1.103            "" =>