diff -r 213dcc39358f -r d9b155757dc8 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue May 13 08:59:21 2003 +0200
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed May 14 10:22:09 2003 +0200
@@ -324,7 +324,7 @@
 apply(  assumption)
 apply( rotate_tac -1)
 apply( simp)
-apply( drule override_SomeD)
+apply( drule map_add_SomeD)
 apply( erule disjE)
 apply(  erule_tac V = "?P --> ?Q" in thin_rl)
 apply (frule map_of_SomeD)
@@ -368,7 +368,7 @@
 apply( clarify)
 apply( subst method_rec)
 apply(  assumption)
-apply( unfold override_def)
+apply( unfold map_add_def)
 apply( simp (no_asm_simp) del: split_paired_Ex)
 apply( case_tac "\<exists>z. map_of(map (\<lambda>(s,m). (s, ?C, m)) ms) sig = Some z")
 apply(  erule exE)
@@ -412,7 +412,7 @@
  apply (subst method_rec)
    apply (assumption)
   apply (assumption)
- apply (simp add: override_def map_of_map split add: option.split)
+ apply (simp add: map_add_def map_of_map split add: option.split)
 done
 
 
@@ -453,7 +453,7 @@
 
 apply clarify
 apply (subgoal_tac "((field (G, D)) ++ map_of (map (\<lambda>(s, f). (s, C, f)) fs)) vn = Some (Da, T)")
-apply (simp (no_asm_use) only:  override_Some_iff)
+apply (simp (no_asm_use) only: map_add_Some_iff)
 apply (erule disjE)
 apply (simp (no_asm_use) add: map_of_map) apply blast
 apply blast