diff -r 6d0392fc6dc5 -r 8dd150d36c65 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Feb 27 18:21:42 2003 +0100
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Thu Feb 27 18:22:49 2003 +0100
@@ -465,7 +465,7 @@
 
 (* case v1 = v2 *)
 apply (rule_tac "instrs1.0" = "[LitPush (Bool True)]" in jump_fwd_progression)
-apply (auto simp: NatBin.nat_add_distrib)
+apply (auto simp: nat_add_distrib)
 apply (rule progression_one_step) apply simp
 
 (* case v1 \<noteq> v2 *)
@@ -474,7 +474,7 @@
 apply (rule progression_one_step [THEN HOL.refl [THEN progression_transitive], simplified]) 
 apply auto
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
-apply (auto simp: NatBin.nat_add_distrib intro: progression_refl)
+apply (auto simp: nat_add_distrib intro: progression_refl)
 done
 
 
@@ -1008,14 +1008,14 @@
 apply fast
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply simp apply (rule conjI, simp) apply (simp add: NatBin.nat_add_distrib)
+apply simp apply (rule conjI, simp) apply (simp add: nat_add_distrib)
 apply (rule progression_refl)
 
  (* case b= False *)
 apply simp
 apply (rule_tac "instrs1.0" = "compStmt (gmb G CL S) c2" in jump_fwd_progression)
 apply (simp, rule conjI, (rule HOL.refl)+)
-apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply fast
 
 (* case exit Loop *)
@@ -1043,7 +1043,7 @@
 apply fast
 apply (rule_tac "instrs1.0" = "[]" in jump_fwd_progression)
 apply (simp, rule conjI, rule HOL.refl, rule HOL.refl)
-apply (simp, rule conjI, rule HOL.refl, simp add: NatBin.nat_add_distrib)
+apply (simp, rule conjI, rule HOL.refl, simp add: nat_add_distrib)
 apply (rule progression_refl)