--- 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

--- a/Nominal/nominal_library.ML	Wed Dec 22 12:17:49 2010 +0000
+++ b/Nominal/nominal_library.ML	Wed Dec 22 12:47:09 2010 +0000
@@ -163,13 +163,7 @@
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
 
 
-
-fun mk_id trm =
-  let 
-    val ty = fastype_of trm
-  in
-    Const (@{const_name id}, ty --> ty) $ trm
-  end
+fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm
 
 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)