diff -r 6fe4200532b7 -r 7071b017cb35 src/HOL/MetisExamples/BT.thy
--- a/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:12 2009 +0100
+++ b/src/HOL/MetisExamples/BT.thy	Fri Jan 16 14:58:56 2009 +0100
@@ -84,7 +84,7 @@
 lemma depth_reflect: "depth (reflect t) = depth t"
   apply (induct t)
   apply (metis depth.simps(1) reflect.simps(1))
-  apply (metis depth.simps(2) min_max.less_eq_less_sup.sup_commute reflect.simps(2))
+  apply (metis depth.simps(2) min_max.sup_commute reflect.simps(2))
   done
 
 text {*