--- a/src/HOL/Library/Efficient_Nat.thy Wed Sep 23 13:42:53 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Sep 23 14:00:12 2009 +0200
@@ -415,9 +415,9 @@
text {* Evaluation *}
lemma [code, code del]:
- "(Code_Eval.term_of \<Colon> nat \<Rightarrow> term) = Code_Eval.term_of" ..
+ "(Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term) = Code_Evaluation.term_of" ..
-code_const "Code_Eval.term_of \<Colon> nat \<Rightarrow> term"
+code_const "Code_Evaluation.term_of \<Colon> nat \<Rightarrow> term"
(SML "HOLogic.mk'_number/ HOLogic.natT")