# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1293022029 0
# Node ID 81921f8ad24553fb6344c23a35303009bd758bfc
# Parent  25fb0dbe9f13b6ce1147f52a39ecf9cd62e5b695
updated to Isabelle 22 December

diff -r 25fb0dbe9f13 -r 81921f8ad245 Nominal/nominal_eqvt.ML
--- 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
diff -r 25fb0dbe9f13 -r 81921f8ad245 Nominal/nominal_library.ML
--- 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)