diff --git a/src/num/theories/arithmeticScript.sml b/src/num/theories/arithmeticScript.sml
index f951878444..9ca58af265 100644
--- a/src/num/theories/arithmeticScript.sml
+++ b/src/num/theories/arithmeticScript.sml
@@ -224,11 +224,6 @@ val NRC = new_recursive_definition {
   def = “(NRC R 0 x y = (x = y)) /\
           (NRC R (SUC n) x y = ?z. R x z /\ NRC R n z y)”};
 
-val bool_to_bit_def = new_definition(
-  "bool_to_bit_def",
-  “bool_to_bit b = if b then 1 else 0”
-);
-
 val _ = overload_on ("RELPOW", “NRC”)
 val _ = overload_on ("NRC", “NRC”)
 
@@ -5002,34 +4997,4 @@ val MOD_EXP = store_thm(
   `_ = (a * a ** m) MOD n` by rw[MOD_TIMES2] >>
   rw[EXP]);
 
-Theorem ODD_bool_to_bit[simp]:
-  ODD (bool_to_bit b) = b /\
-  ODD (1 - bool_to_bit b) = ~b
-Proof
-  rw[bool_to_bit_def, ODD, ONE, SUB_MONO_EQ, SUB_0]
-QED
-
-Theorem bool_to_bit_neq_add:
-  bool_to_bit (x <> y) =
-  (bool_to_bit x + bool_to_bit y) MOD 2
-Proof
-  reverse(rw[bool_to_bit_def, ADD_0, ADD])
-  >- (
-    rw[ONE, ADD] \\ rw[GSYM TWO, GSYM ONE]
-    \\ irule EQ_SYM
-    \\ irule (DIVMOD_ID |> SPEC_ALL |> UNDISCH |> cj 2 |> DISCH_ALL)
-    \\ rw[TWO, LESS_0] )
-  \\ irule EQ_SYM
-  \\ irule ONE_MOD
-  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
-QED
-
-Theorem bool_to_bit_MOD_2[simp]:
-  bool_to_bit x MOD 2 = bool_to_bit x
-Proof
-  rw[bool_to_bit_def]
-  \\ irule ONE_MOD
-  \\ rw[ONE, TWO, LESS_MONO, LESS_0]
-QED
-
 val _ = export_theory()