diff -r 620a5d8cfa78 -r 7a91c7bcfe7e src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Aug 28 19:35:49 2009 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Aug 28 19:43:19 2009 +0200
@@ -918,8 +918,8 @@
   apply (frule asm_rl)
   apply (drule spec)
   apply (erule trans)
-  apply (drule_tac x = "bin_cat y n a" in spec) 
-  apply (simp add : bin_cat_assoc_sym min_def)
+  apply (drule_tac x = "bin_cat y n a" in spec)
+  apply (simp add : bin_cat_assoc_sym)
   done
 
 lemma bin_rcat_bl: