fix

--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Apr 21 17:22:17 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Apr 21 17:22:23 2005 +0200
@@ -907,9 +907,6 @@
   \<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))"
 by (simp add: check_type_def states_lower)
 
-lemma max_same_iter [simp]: "max (x::'a::linorder) (max x y) = max x y"
-by (simp add: AC_max.assoc [THEN sym])
-
   (* ******************************************************************* *)
 
 constdefs