--- a/Nominal/nominal_eqvt.ML	Wed Dec 22 12:17:49 2010 +0000
+++ b/Nominal/nominal_eqvt.ML	Wed Dec 22 12:47:09 2010 +0000
@@ -21,7 +21,7 @@
 open Nominal_ThmDecls;
 
 val atomize_conv = 
-  MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
+  Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
     (HOL_basic_ss addsimps @{thms induct_atomize});
 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1