Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_inductive2.ML
changeset 34918 81c7ec7c1b91
parent 33968 f94fb13ecbb3
child 35232 f588e1169c8b 
--- 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
isabelle