1.1 --- a/src/HOL/Library/Code_Integer.thy	Wed Sep 23 13:42:53 2009 +0200
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Wed Sep 23 14:00:12 2009 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  
     1.5  text {* Evaluation *}
     1.6  
     1.7 -code_const "Code_Eval.term_of \<Colon> int \<Rightarrow> term"
     1.8 +code_const "Code_Evaluation.term_of \<Colon> int \<Rightarrow> term"
     1.9    (Eval "HOLogic.mk'_number/ HOLogic.intT")
    1.10  
    1.11  end
    1.12 \ No newline at end of file