--- a/thys/TM_Assemble.thy	Fri Mar 21 13:49:20 2014 +0000
+++ b/thys/TM_Assemble.thy	Fri Mar 21 15:07:59 2014 +0000
@@ -868,7 +868,7 @@
       assume h[rule_format]:
         "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i"
       from h1 h3 have p1: "l < length (sts' - sts)"
-        by (metis length_list_update min_max.inf.idem minus_list_len)
+        by (metis length_list_update min.idem minus_list_len)
       from p1 h2 h3 have p2: "(sts' - sts)!l = Bound"
         by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus)
       from h[OF p1 p2] have "(<(i = x ! l)>) 0" 
@@ -1674,7 +1674,7 @@
 proof(induct rule:nth_equalityI)
   case 1
   show ?case
-    by (metis min_max.inf.commute plus_list_len)
+    by (metis min.commute plus_list_len)
 next
   case 2
   { fix i