set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 05 08:24:28 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Mar 06 11:10:18 2009 +0100
@@ -201,7 +201,7 @@
           | add_set (t, T) ((u, U) :: ps) =
               if T = U then
                 let val S = HOLogic.mk_setT T
-                in (Const (@{const_name "op Un"}, S --> S --> S) $ u $ t, T) :: ps
+                in (Const (@{const_name "Un"}, S --> S --> S) $ u $ t, T) :: ps
                 end
               else (u, U) :: add_set (t, T) ps
       in