src/HOL/Tools/BNF/bnf_util.ML
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);