--- a/src/HOL/Library/Word.thy Sat Mar 29 19:24:57 2008 +0100
+++ b/src/HOL/Library/Word.thy Sat Mar 29 22:55:49 2008 +0100
@@ -2325,8 +2325,7 @@
(*lcp** val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f *)
val simproc2 = Simplifier.simproc @{theory} "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
in
- (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2]);
- thy))
+ Simplifier.map_simpset (fn ss => ss addsimprocs [(*lcp*simproc1,*)simproc2])
end*}
declare bv_to_nat1 [simp del]