src/HOL/Word/Bool_List_Representation.thy

   "takefill fill (m + length xs) (xs @ w) = xs @ (takefill fill m w)"
   by (induct xs) auto
 
 lemma takefill_same': 
   "l = length xs ==> takefill fill l xs = xs"
-  by clarify (induct xs, auto)
+  by (induct xs arbitrary: l, auto)
  
 lemmas takefill_same [simp] = takefill_same' [OF refl]
 
 lemma takefill_bintrunc:
   "takefill False n bl = rev (bin_to_bl n (bl_to_bin (rev bl)))"