diff -r 82acc20ded73 -r a064732223ad src/HOL/IMP/Sec_TypingT.thy
--- a/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/IMP/Sec_TypingT.thy	Wed Dec 25 17:39:07 2013 +0100
@@ -190,7 +190,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 While')