diff -r 056255ade52a -r 4e74209f113e src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Library/List_Prefix.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -15,10 +15,10 @@
 begin
 
 definition
-  prefix_def [code func del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
+  prefix_def [code del]: "xs \<le> ys = (\<exists>zs. ys = xs @ zs)"
 
 definition
-  strict_prefix_def [code func del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
+  strict_prefix_def [code del]: "xs < ys = (xs \<le> ys \<and> xs \<noteq> (ys::'a list))"
 
 instance
   by intro_classes (auto simp add: prefix_def strict_prefix_def)
@@ -374,18 +374,18 @@
 
 subsection {* Executable code *}
 
-lemma less_eq_code [code func]:
+lemma less_eq_code [code]:
     "([]\<Colon>'a\<Colon>{eq, ord} list) \<le> xs \<longleftrightarrow> True"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> [] \<longleftrightarrow> False"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs \<le> y # ys \<longleftrightarrow> x = y \<and> xs \<le> ys"
   by simp_all
 
-lemma less_code [code func]:
+lemma less_code [code]:
     "xs < ([]\<Colon>'a\<Colon>{eq, ord} list) \<longleftrightarrow> False"
     "[] < (x\<Colon>'a\<Colon>{eq, ord})# xs \<longleftrightarrow> True"
     "(x\<Colon>'a\<Colon>{eq, ord}) # xs < y # ys \<longleftrightarrow> x = y \<and> xs < ys"
   unfolding strict_prefix_def by auto
 
-lemmas [code func] = postfix_to_prefix
+lemmas [code] = postfix_to_prefix
 
 end