diff -r 35807a5d8dc2 -r 2a1953f0d20d src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Semiring_Normalization.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -116,7 +116,8 @@
   "x ^ (Suc q) = x * (x ^ q)"
   "x ^ (2*n) = (x ^ n) * (x ^ n)"
   "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))"
-  by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult)
+  by (simp_all add: algebra_simps power_add power2_eq_square
+    power_mult_distrib power_mult del: one_add_one)
 
 lemmas normalizing_comm_semiring_1_axioms =
   comm_semiring_1_axioms [normalizer
@@ -218,4 +219,13 @@
 
 hide_fact (open) normalizing_field_axioms normalizing_field_ops normalizing_field_rules
 
+code_modulename SML
+  Semiring_Normalization Arith
+
+code_modulename OCaml
+  Semiring_Normalization Arith
+
+code_modulename Haskell
+  Semiring_Normalization Arith
+
 end