# HG changeset patch
# User huffman
# Date 1221840319 -7200
# Node ID 3eb2855e54028666d6b83f608666e3b49ad2941e
# Parent  107ba67497a1f825f0640e1b61864eeeefebd614
avoid using implicit assumptions

diff -r 107ba67497a1 -r 3eb2855e5402 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Sep 19 17:54:04 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Sep 19 18:05:19 2008 +0200
@@ -1116,7 +1116,7 @@
 proof (induct n nw w cs arbitrary: v bs rule: bin_rsplit_aux.induct)
   case (1 n m w cs v bs) show ?case
   proof (cases "m = 0")
-    case True then show ?thesis by simp
+    case True then show ?thesis using `length bs = length cs` by simp
   next
     case False
     from "1.hyps" `m \<noteq> 0` `n \<noteq> 0` have hyp: "\<And>v bs. length bs = Suc (length cs) \<Longrightarrow>