diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Wed May 14 10:22:09 2003 +0200
@@ -254,7 +254,7 @@
 apply (rule inv_f_eq) apply (simp add: inj_on_def) apply simp
 
 apply (intro strip)
-apply (simp add: override_Some_iff map_of_map del: split_paired_Ex)
+apply (simp add: map_add_Some_iff map_of_map del: split_paired_Ex)
 apply (subgoal_tac "\<forall>x\<in>set ms. fst ((Fun.comp (\<lambda>(s, m). (s, Ca, m)) (compMethod G Ca)) x) = fst x")
 (*
 apply (subgoal_tac "\<forall>x\<in>set ms. fst (((\<lambda>(s, m). (s, Ca, m)) \<circ> compMethod G Ca) x) = fst x")
@@ -329,14 +329,14 @@
 apply (case_tac "(method (G, D) ++  map_of (map (\<lambda>(s, m). (s, C, m)) ms)) S")
 
   (* case None *)
-apply (simp (no_asm_simp) add: override_None)
+apply (simp (no_asm_simp) add: map_add_None)
 apply (simp add: map_of_map_compMethod comp_method_result_def) 
 
   (* case Some *)
-apply (simp add: override_Some_iff)
+apply (simp add: map_add_Some_iff)
 apply (erule disjE)
   apply (simp add: split_beta map_of_map_compMethod)
-  apply (simp add: override_def comp_method_result_def map_of_map_compMethod)
+  apply (simp add: map_add_def comp_method_result_def map_of_map_compMethod)
 
   (* show subgoals *)
 apply (simp add: comp_subcls1)