diff -r 9c4f4ac0d038 -r d8e4cd2ac2a1 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 05 08:23:10 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 05 08:23:11 2009 +0100
@@ -70,7 +70,7 @@
   | add_binders thy i (Abs (_, _, t)) bs = add_binders thy (i + 1) t bs
   | add_binders thy i _ bs = bs;
 
-fun mk_set T [] = Const ("{}", HOLogic.mk_setT T)
+fun mk_set T [] = Const (@{const_name Set.empty}, HOLogic.mk_setT T)
   | mk_set T (x :: xs) =
       Const ("insert", T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $
         mk_set T xs;