# HG changeset patch
# User nipkow
# Date 1114010382 -7200
# Node ID 70d559802ae397109d4f32737a49decb26db339e
# Parent  6744bba5561d5c5739aeb32edea2de59406de0aa
Used locale interpretations everywhere. -> lemma had new name

diff -r 6744bba5561d -r 70d559802ae3 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Apr 20 17:19:18 2005 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Wed Apr 20 17:19:42 2005 +0200
@@ -908,7 +908,7 @@
 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 del: max_assoc add: max_assoc [THEN sym])
+by (simp add: AC_max.assoc [THEN sym])
 
   (* ******************************************************************* *)