diff -r cd747b068311 -r cedf2ac63d9c src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Sep 01 15:01:12 2010 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Sep 01 15:01:13 2010 +0200
@@ -92,7 +92,7 @@
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>
-      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
+      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym))
   end;
 
 fun add_functrans (name, f) = (map_data o apsnd)