# HG changeset patch
# User haftmann
# Date 1291296878 -3600
# Node ID 3113fd4810bd0e4649d13d5c25359f87e9ebabd7
# Parent  b37dca06477ff6e280843e619aff5a5fe56a1a3f
corrected representation for code_numeral numerals

diff -r b37dca06477f -r 3113fd4810bd src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Thu Dec 02 13:53:36 2010 +0100
+++ b/src/HOL/Code_Evaluation.thy	Thu Dec 02 14:34:38 2010 +0100
@@ -153,7 +153,7 @@
   by (simp only: term_of_anything)
 
 lemma (in term_syntax) term_of_code_numeral_code [code]:
-  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num (2::code_numeral) k"
+  "term_of (k::code_numeral) = termify (number_of :: int \<Rightarrow> code_numeral) <\<cdot>> term_of_num_semiring (2::code_numeral) k"
   by (simp only: term_of_anything)
 
 definition term_of_num_ring :: "'a\<Colon>ring_div \<Rightarrow> 'a \<Rightarrow> term" where