src/HOL/Induct/LList.thy

--- a/src/HOL/Induct/LList.thy	Mon May 09 16:02:45 2005 +0200
+++ b/src/HOL/Induct/LList.thy	Mon May 09 16:38:56 2005 +0200
@@ -865,7 +865,8 @@
        in llist_equalityI)
  apply (rule rangeI)
 apply (safe)
-apply (simplesubst iterates, simp)  --{*two redexes*}
+apply (subst (1 2) iterates)
+apply simp 
 done
 
 subsubsection{* Two proofs that @{text lmap} distributes over lappend *}