1.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4  
     1.5  text {* Evaluation *}
     1.6  
     1.7 -lemma [code func, code func del]:
     1.8 +lemma [code, code del]:
     1.9    "(Code_Eval.term_of \<Colon> int \<Rightarrow> term) = Code_Eval.term_of" ..
    1.10  
    1.11  code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"