diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
+++ b/src/HOL/UNITY/Simple/Common.thy	Wed Dec 25 17:39:06 2013 +0100
@@ -65,7 +65,7 @@
 lemma "mk_total_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV)
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
 done
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
@@ -73,7 +73,7 @@
           (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)   
        \<in> {m} co (maxfg m)"
 apply (simp add: mk_total_program_def) 
-apply (simp add: constrains_def maxfg_def gasc min_max.sup_absorb2)
+apply (simp add: constrains_def maxfg_def gasc max.absorb2)
 done