diff -r f89c0749533d -r dde0e76996ad src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jul 24 18:46:38 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Thu Jul 24 18:46:38 2014 +0200
@@ -121,16 +121,16 @@
 
 fun chain_qs_lfs NONE lfs = ([], lfs)
   | chain_qs_lfs (SOME l0) lfs =
-    if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
+    if member (op =) lfs l0 then ([Then], remove (op =) l0 lfs) else ([], lfs)
+
 fun chain_isar_step lbl (Prove (qs, xs, l, t, subs, (lfs, gfs), meths, comment)) =
     let val (qs', lfs) = chain_qs_lfs lbl lfs in
       Prove (qs' @ qs, xs, l, t, map chain_isar_proof subs, (lfs, gfs), meths, comment)
     end
   | chain_isar_step _ step = step
 and chain_isar_steps _ [] = []
-  | chain_isar_steps (prev as SOME _) (i :: is) =
+  | chain_isar_steps prev (i :: is) =
     chain_isar_step prev i :: chain_isar_steps (label_of_isar_step i) is
-  | chain_isar_steps _ (i :: is) = i :: chain_isar_steps (label_of_isar_step i) is
 and chain_isar_proof (Proof (fix, assms, steps)) =
   Proof (fix, assms, chain_isar_steps (try (List.last #> fst) assms) steps)