1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -121,16 +121,16 @@
     1.4  
     1.5  fun chain_qs_lfs NONE lfs = ([], lfs)
     1.6    | chain_qs_lfs (SOME l0) lfs =
     1.7 -    if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
     1.8 +    if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
     1.9 +
    1.10  fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
    1.11      let val (qs', lfs) = chain_qs_lfs lbl lfs in
    1.12        Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
    1.13      end
    1.14    | chain_isar_step _ step = step
    1.15  and chain_isar_steps _ [] = []
    1.16 -  | chain_isar_steps (prev as SOME _) (i :: is) =
    1.17 +  | chain_isar_steps prev (i :: is) =
    1.18      chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
    1.19 -  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
    1.20  and chain_isar_proof (Proof (fix, assms, steps)) =
    1.21    Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)
    1.22