diff -r 91c05f4b509e -r 5f9138bcb3d7 src/HOL/Library/Pure_term.thy
--- a/src/HOL/Library/Pure_term.thy	Sun May 06 21:49:44 2007 +0200
+++ b/src/HOL/Library/Pure_term.thy	Sun May 06 21:50:17 2007 +0200
@@ -92,8 +92,8 @@
 
 code_datatype Const App Fix Absp Bound
 lemmas [code func] = Bnd_Bound Abs_Absp
-lemmas [code nofunc] = term.recs term.cases term.size
-lemma [code func, code nofunc]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
+lemmas [code func del] = term.recs term.cases term.size
+lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
 
 code_type "typ" and "term"
   (SML "Term.typ" and "Term.term")