repaired attribute code_unfold_post which has ever been broken
authorhaftmann
Wed, 01 Sep 2010 15:01:13 +0200
changeset 38973 cedf2ac63d9c
parent 38972 cd747b068311
child 38974 e109feb514a8
repaired attribute code_unfold_post which has ever been broken
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)