src/HOL/List.thy

--- a/src/HOL/List.thy	Wed Feb 02 18:06:25 2005 +0100
+++ b/src/HOL/List.thy	Wed Feb 02 18:19:43 2005 +0100
@@ -582,7 +582,7 @@
 
 lemma rev_induct [case_names Nil snoc]:
   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
-apply(subst rev_rev_ident[symmetric])
+apply(simplesubst rev_rev_ident[symmetric])
 apply(rule_tac list = "rev xs" in list.induct, simp_all)
 done