diff -r bd4ecd48c21f -r adcb9a1198e7 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Dec 17 13:45:43 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Fri Dec 17 14:09:37 2010 +0100
@@ -83,10 +83,10 @@
 val map_pre = map_pre_post o apfst;
 val map_post = map_pre_post o apsnd;
 
-val add_unfold = map_pre o MetaSimplifier.add_simp;
-val del_unfold = map_pre o MetaSimplifier.del_simp;
-val add_post = map_post o MetaSimplifier.add_simp;
-val del_post = map_post o MetaSimplifier.del_simp;
+val add_unfold = map_pre o Simplifier.add_simp;
+val del_unfold = map_pre o Simplifier.del_simp;
+val add_post = map_post o Simplifier.add_simp;
+val del_post = map_post o Simplifier.del_simp;
 
 fun add_unfold_post raw_thm thy =
   let
@@ -94,7 +94,7 @@
     val thm_sym = Thm.symmetric thm;
   in
     thy |> map_pre_post (fn (pre, post) =>
-      (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.add_simp thm_sym))
+      (pre |> Simplifier.add_simp thm, post |> Simplifier.add_simp thm_sym))
   end;
 
 fun add_functrans (name, f) = (map_data o apsnd)