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