# HG changeset patch
# User berghofe
# Date 1263579291 -3600
# Node ID 81c7ec7c1b9103f5b7359b3a77d7e9f28063898a
# Parent  51829fe604a70a7babc91f07e69d3ab55728d9be
union is an abbreviation for sup.

diff -r 51829fe604a7 -r 81c7ec7c1b91 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 15 14:43:00 2010 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Jan 15 19:14:51 2010 +0100
@@ -196,7 +196,7 @@
           | add_set (t, T) ((u, U) :: ps) =
               if T = U then
                 let val S = HOLogic.mk_setT T
-                in (Const (@{const_name union}, S --> S --> S) $ u $ t, T) :: ps
+                in (Const (@{const_name sup}, S --> S --> S) $ u $ t, T) :: ps
                 end
               else (u, U) :: add_set (t, T) ps
       in