src/HOL/Word/Word.thy

--- a/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
+++ b/src/HOL/Word/Word.thy	Thu Oct 31 11:44:20 2013 +0100
@@ -506,10 +506,6 @@
 definition max_word :: "'a::len word" -- "Largest representable machine integer." where
   "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
 
-primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
-  "of_bool False = 0"
-| "of_bool True = 1"
-
 (* FIXME: only provide one theorem name *)
 lemmas of_nth_def = word_set_bits_def