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)