Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/word_setup.ML
changeset 22578 b0eb5652f210
parent 20485 3078fd2eec7b 
--- a/src/HOL/Library/word_setup.ML	Wed Apr 04 00:10:59 2007 +0200
+++ b/src/HOL/Library/word_setup.ML	Wed Apr 04 00:11:03 2007 +0200
@@ -35,8 +35,8 @@
 		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
 		else NONE
 	      | g _ _ _ = NONE
-  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
-	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
+  (*lcp**	    val simproc1 = Simplifier.simproc thy "nat_to_bv" ["Word.nat_to_bv (number_of w)"] f ***)
+	    val simproc2 = Simplifier.simproc thy "bv_to_nat" ["Word.bv_to_nat (x # xs)"] g
 	in
 	  Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [(*lcp*simproc1,**)simproc2]);
           thy
isabelle