diff -r 7187bce94e88 -r ac4a2a66707d src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:06:15 2011 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 21 14:25:38 2011 +0200
@@ -74,7 +74,7 @@
 next
   assume "xs = ys @ [y] \<or> xs \<le> ys"
   then show "xs \<le> ys @ [y]"
-    by (metis order_eq_iff strict_prefixE strict_prefixI' xt1(7))
+    by (metis order_eq_iff order_trans prefixI)
 qed
 
 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)"