diff -r c5cb19ecbd41 -r 1e6d86821718 src/Tools/Code/code_simp.ML
--- a/src/Tools/Code/code_simp.ML	Fri Dec 17 18:24:44 2010 +0100
+++ b/src/Tools/Code/code_simp.ML	Fri Dec 17 18:33:35 2010 +0100
@@ -24,7 +24,7 @@
 (
   type T = simpset;
   val empty = empty_ss;
-  fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
+  fun extend ss = Simplifier.inherit_context empty_ss ss;
   val merge = merge_ss;
 );