# HG changeset patch
# User huffman
# Date 1330009756 -3600
# Node ID a8c342aa53d6e72beaf53ccb85651f309bde5516
# Parent  8c5d10d4139125a138e526f5778b6fb561e11b1e
make more simp rules respect int/bin distinction

diff -r 8c5d10d41391 -r a8c342aa53d6 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Feb 23 15:37:42 2012 +0100
+++ b/src/HOL/Word/Word.thy	Thu Feb 23 16:09:16 2012 +0100
@@ -779,8 +779,8 @@
   unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
 
 lemma to_bl_no_bin [simp]:
-  "to_bl (number_of bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
-  by (fact to_bl_of_bin [folded word_number_of_def])
+  "to_bl (number_of bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) (number_of bin)"
+  unfolding word_number_of_alt by (rule to_bl_of_bin)
 
 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   unfolding uint_bl by (simp add : word_size)
@@ -3251,12 +3251,12 @@
 subsubsection "Slices"
 
 lemma slice1_no_bin [simp]:
-  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
+  "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (number_of w)))"
   by (simp add: slice1_def)
 
 lemma slice_no_bin [simp]:
   "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
-    (bin_to_bl (len_of TYPE('b :: len0)) w))"
+    (bin_to_bl (len_of TYPE('b :: len0)) (number_of w)))"
   by (simp add: slice_def word_size)
 
 lemma slice1_0 [simp] : "slice1 n 0 = 0"