# HG changeset patch
# User haftmann
# Date 1283346073 -7200
# Node ID cedf2ac63d9cb9d5917735dbd9235e3b20e63dd9
# Parent  cd747b068311556d13a0e64d4d41c07491f34a3a
repaired attribute code_unfold_post which has ever been broken

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)