changeset 56218 | 1c3f1f2431f9 |
parent 55945 | e96383acecf9 |
child 56521 | 20cfb18a53ba |
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Mar 19 17:06:02 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Mar 19 18:47:22 2014 +0100 @@ -393,7 +393,7 @@ fun mk_UNION X f = let val (T, U) = dest_funT (fastype_of f); - in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end; + in Const (@{const_name SUPREMUM}, fastype_of X --> (T --> U) --> U) $ X $ f end; fun mk_Union T = Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);