diff -r cb3612cc41a3 -r fc075ae929e4 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Sun Jan 30 20:48:50 2005 +0100
+++ b/src/HOL/UNITY/ListOrder.thy	Tue Feb 01 18:01:57 2005 +0100
@@ -215,8 +215,7 @@
 apply (erule disjE)
 apply (simp_all (no_asm_simp) add: neq_Nil_conv nth_append)
 apply (blast intro: genPrefix.append, auto)
-apply (subst append_cons_eq)
-apply (blast intro: genPrefix_append_both genPrefix.append)
+apply (subst append_cons_eq, fast intro: genPrefix_append_both genPrefix.append)
 done
 
 lemma append_one_genPrefix: