diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -47,7 +47,7 @@
   using assms by (induct rule: less_eq_list.induct) blast+
 
 definition
-  [code func del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
+  [code del]: "(xs \<Colon> 'a list) < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
 
 lemma ileq_length: "xs \<le> ys \<Longrightarrow> length xs \<le> length ys"
   by (induct rule: ileq_induct) auto