diff -r c9cf0780cd4f -r b656af4c9796 src/HOL/Tools/SMT/smt_normalize.ML
--- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:28:10 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 05 11:34:54 2011 +0200
@@ -475,8 +475,7 @@
     "op * = (%a b. nat (int a * int b))"
     "op div = (%a b. nat (int a div int b))"
     "op mod = (%a b. nat (int a mod int b))"
-    by (auto intro!: ext simp add: nat_mult_distrib nat_div_distrib
-      nat_mod_distrib)}
+    by (fastsimp simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
 
   val ints = map mk_meta_eq @{lemma
     "int 0 = 0"