--- a/src/HOL/Tools/hologic.ML Fri Feb 23 17:59:57 2018 +0100
+++ b/src/HOL/Tools/hologic.ML Fri Feb 23 19:25:37 2018 +0100
@@ -10,6 +10,7 @@
val mk_comp: term * term -> term
val boolN: string
val boolT: typ
+ val mk_obj_eq: thm -> thm
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
@@ -187,6 +188,8 @@
(* logic *)
+fun mk_obj_eq th = th RS @{thm meta_eq_to_obj_eq};
+
val Trueprop = Const (\<^const_name>\<open>Trueprop\<close>, boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;