--- a/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:58 2005 +0200
+++ b/src/HOL/Library/word_setup.ML Mon Jun 20 22:13:59 2005 +0200
@@ -24,7 +24,7 @@
fun add_word thy =
let
(*lcp** val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
- val fast2_th = PureThy.get_thm thy ("Word.fast_bv_to_nat_def", NONE)
+ val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
(*lcp** fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
if num_is_usable t
then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)