src/HOL/IMP/Sec_Typing.thy

--- a/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Wed Dec 25 17:39:07 2013 +0100
@@ -200,7 +200,7 @@
 apply (metis Skip')
 apply (metis Assign')
 apply (metis Seq')
-apply (metis min_max.inf_sup_ord(3) max.absorb2 nat_le_linear If' anti_mono')
+apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
 by (metis less_or_eq_imp_le max.absorb1 max.absorb2 nat_le_linear While' anti_mono')