--- a/src/HOL/Tools/hologic.ML Thu Feb 28 16:38:17 2013 +0100
+++ b/src/HOL/Tools/hologic.ML Thu Feb 28 16:54:52 2013 +0100
@@ -15,6 +15,7 @@
val Trueprop: term
val mk_Trueprop: term -> term
val dest_Trueprop: term -> term
+ val Trueprop_conv: conv -> conv
val mk_induct_forall: typ -> term
val mk_setT: typ -> typ
val dest_setT: typ -> typ
@@ -195,13 +196,19 @@
(* logic *)
-val Trueprop = Const ("HOL.Trueprop", boolT --> propT);
+val Trueprop = Const (@{const_name Trueprop}, boolT --> propT);
fun mk_Trueprop P = Trueprop $ P;
-fun dest_Trueprop (Const ("HOL.Trueprop", _) $ P) = P
+fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
| dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+fun Trueprop_conv cv ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct
+ | _ => raise CTERM ("Trueprop_conv", [ct]))
+
+
fun conj_intr thP thQ =
let
val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)