--- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 08 00:43:21 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 08 10:16:37 2016 +0200
@@ -36,6 +36,8 @@
val snd_const: typ -> term
val Id_const: typ -> term
+ val enforce_type: Proof.context -> (typ -> typ) -> typ -> term -> term
+
val mk_Ball: term -> term -> term
val mk_Bex: term -> term -> term
val mk_Card_order: term -> term
@@ -221,6 +223,9 @@
(** Operators **)
+fun enforce_type ctxt get_T T t =
+ Term.subst_TVars (tvar_subst (Proof_Context.theory_of ctxt) [get_T (fastype_of t)] [T]) t;
+
fun mk_converse R =
let
val RT = dest_relT (fastype_of R);