diff -r c65e5cbdbc97 -r 82acc20ded73 src/HOL/Word/Bool_List_Representation.thy --- a/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100 +++ b/src/HOL/Word/Bool_List_Representation.thy Wed Dec 25 17:39:06 2013 +0100 @@ -906,7 +906,7 @@ apply (drule meta_spec) apply (erule trans) apply (drule_tac x = "bin_cat y n a" in meta_spec) - apply (simp add : bin_cat_assoc_sym min_max.inf_absorb2) + apply (simp add : bin_cat_assoc_sym min.absorb2) done lemma bin_rcat_bl: