--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Sep 12 09:29:25 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Sep 12 13:35:29 2016 +0200
@@ -70,6 +70,7 @@
val mk_reflp: term -> term
val mk_symp: term -> term
val mk_transp: term -> term
+ val mk_union: term * term -> term
(*parameterized terms*)
val mk_nthN: int -> term -> int -> term
@@ -281,6 +282,8 @@
fun mk_Union T =
Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T);
+val mk_union = HOLogic.mk_binop @{const_name sup};
+
fun mk_Field r =
let val T = fst (dest_relT (fastype_of r));
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;