# HG changeset patch
# User haftmann
# Date 1236334218 -3600
# Node ID 8f4d5eaa98789e18e746fbe27659f247d3a7c9ff
# Parent  720226bedc4d7eb12443c5c7625afa2cf924623e
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax

diff -r 720226bedc4d -r 8f4d5eaa9878 src/HOL/Nominal/nominal_inductive2.ML
--- 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