diff -r 6f012a209dac -r c8a9eaaa2f59 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Oct 22 23:45:20 2010 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Sun Oct 24 20:19:00 2010 +0200
@@ -258,7 +258,7 @@
 lemma bounded_append [simp]:
   "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
   apply (simp add: check_bounded_def)
-  apply (simp add: nat_number append_ins_def)
+  apply (simp add: eval_nat_numeral append_ins_def)
   apply (rule allI, rule impI)
   apply (elim pc_end pc_next pc_0)
   apply auto
@@ -327,7 +327,7 @@
 
 lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
   apply (simp add: check_bounded_def)
-  apply (simp add: nat_number make_list_ins_def)
+  apply (simp add: eval_nat_numeral make_list_ins_def)
   apply (rule allI, rule impI)
   apply (elim pc_end pc_next pc_0)
   apply auto
@@ -343,7 +343,7 @@
   "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
   apply (simp add: wt_method_def)
   apply (simp add: make_list_ins_def phi_makelist_def)
-  apply (simp add: wt_start_def nat_number)
+  apply (simp add: wt_start_def eval_nat_numeral)
   apply (simp add: wt_instr_def)
   apply clarify
   apply (elim pc_end pc_next pc_0)