diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -442,7 +442,7 @@
 (********************************************************************************)
 
 lemma max_of_list_elem: "x \<in> set xs \<Longrightarrow> x \<le> (max_of_list xs)"
-by (induct xs, auto intro: le_maxI1 simp: le_max_iff_disj max_of_list_def)
+by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
 
 lemma max_of_list_sublist: "set xs \<subseteq> set ys 
   \<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
@@ -1053,7 +1053,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 eff_def norm_eff_def min_max.sup_absorb2)
+    max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
 apply (intro strip)
 apply (rule conjI)
 apply (rule check_type_mono, assumption, simp)
@@ -1064,7 +1064,7 @@
   bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
   apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
   apply (simp add: max_ssize_def ssize_sto_def max_of_list_def) 
-  apply (simp add: check_type_simps min_max.sup_absorb1)
+  apply (simp add: check_type_simps max.absorb1)
   apply clarify
   apply (rule_tac x="(length ST)" in exI)
   apply simp+
@@ -1087,7 +1087,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 eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1106,7 +1106,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 eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1124,7 +1124,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 eff_def norm_eff_def min_max.sup_absorb2)
+            max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1148,7 +1148,7 @@
   apply (simp add: max_ssize_def  max_of_list_def)
   apply (simp add: ssize_sto_def)
   apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule conjI)
 apply (rule_tac x="(length ST)" in exI)
@@ -1162,7 +1162,7 @@
   apply (simp add: sup_state_conv)
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
  apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule_tac x="(length ST)" in exI)
 apply simp+
@@ -1172,7 +1172,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 eff_def norm_eff_def min_max.sup_absorb2)
+             max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1185,7 +1185,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 eff_def norm_eff_def min_max.sup_absorb2)
+              max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
   apply (intro strip)
   apply (rule conjI)
   apply (rule check_type_mono, assumption, simp)
@@ -1202,7 +1202,7 @@
          (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)
-  apply (simp add: check_type_simps min_max.sup_absorb1)
+  apply (simp add: check_type_simps max.absorb1)
   apply clarify
   apply (rule_tac x="Suc (length ST)" in exI)
   apply simp+
@@ -1245,7 +1245,7 @@
   apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
 
   apply (intro strip)
-apply (simp add: check_type_simps min_max.sup_absorb1)
+apply (simp add: check_type_simps max.absorb1)
 apply clarify
 apply (rule_tac x="Suc (length ST)" in exI)
 apply simp+