diff -r 87d98857d154 -r 16464c3f86bd src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 20:07:11 2009 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Fri Aug 28 20:18:33 2009 +0200
@@ -959,7 +959,7 @@
 apply simp
 apply (simp (no_asm_simp))+
 apply simp
-apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp) add: max_def)
+apply (simp add: max_ssize_def max_of_list_append) apply (simp (no_asm_simp))
 
   (* show check_type \<dots> *)
 apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
@@ -973,7 +973,7 @@
 apply (simp add: check_type_def)
 apply (rule states_lower, assumption)
 apply (simp (no_asm_simp) add: max_ssize_def max_of_list_append)
-apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
 apply (simp (no_asm_simp))+
 done
 
@@ -988,7 +988,7 @@
 apply (drule_tac x=sttp in spec, erule exE)
 apply simp
 apply (rule check_type_mono, assumption)
-apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def split: prod.split)
+apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
 done
 
   (* ********************************************************************** *)
@@ -1058,8 +1058,7 @@
 lemma bc_mt_corresp_New: "\<lbrakk>is_class cG cname \<rbrakk>
   \<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-    max_ssize_def max_of_list_def ssize_sto_def max_def 
-    eff_def norm_eff_def)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1081,7 +1080,7 @@
   \<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
   apply (erule exE)+
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length STo)" in exI)
@@ -1093,8 +1092,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1113,8 +1111,7 @@
   \<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
 apply (subgoal_tac "\<exists> ST LT. sttp= (ST, LT)", (erule exE)+)
   apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1130,8 +1127,7 @@
   \<Longrightarrow> bc_mt_corresp [Load i] 
          (\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
 apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1180,8 +1176,7 @@
 lemma bc_mt_corresp_Dup: "
   bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
  apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1194,8 +1189,7 @@
 lemma bc_mt_corresp_Dup_x1: "
   bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
-                 max_ssize_def max_of_list_def ssize_sto_def max_def
-                 eff_def norm_eff_def)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1211,7 +1205,7 @@
   bc_mt_corresp [IAdd] (replST 2 (PrimT Integer)) 
          (PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
   apply (simp add: check_type_simps)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
@@ -1252,7 +1246,7 @@
   apply (frule widen_field, assumption+)
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
-  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def max_def)
+  apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
 apply (simp add: check_type_simps)
@@ -1303,7 +1297,7 @@
   apply (simp add: max_spec_preserves_length [THEN sym])
 
   -- "@{text check_type}"
-apply (simp add: max_ssize_def ssize_sto_def max_def)
+apply (simp add: max_ssize_def ssize_sto_def)
 apply (simp add: max_of_list_def)
 apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
 apply simp
@@ -1314,7 +1308,7 @@
 apply (simp only: comp_is_type)
 apply (frule method_wf_mdecl) apply assumption apply assumption
 apply (simp add: wf_mdecl_def wf_mhead_def)
-apply (simp add: max_def)
+apply (simp)
   done
 
 
@@ -1471,7 +1465,7 @@
 apply (case_tac "sttp1", simp)
 apply (rule check_type_lower) apply assumption
 apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
-apply (simp (no_asm_simp) add: max_of_list_def max_def)
+apply (simp (no_asm_simp) add: max_of_list_def)
 
   (* subgoals \<exists> ... *)
 apply (rule surj_pair)+