diff -r 102a0a0718c5 -r eac4bb5adbf9 src/HOL/Tools/hologic.ML
--- 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)