added Trueprop_conv

--- a/src/HOL/hologic.ML	Mon Nov 27 13:42:42 2006 +0100
+++ b/src/HOL/hologic.ML	Mon Nov 27 13:42:46 2006 +0100
@@ -18,6 +18,7 @@
   val Trueprop: term
   val mk_Trueprop: term -> term
   val dest_Trueprop: term -> term
+  val Trueprop_conv: (cterm -> thm) -> cterm -> thm
   val conj: term
   val disj: term
   val imp: term
@@ -131,6 +132,11 @@
 fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
   | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
 
+fun Trueprop_conv conv ct = (case term_of ct of
+    Const ("Trueprop", _) $ _ =>
+      let val (ct1, ct2) = Thm.dest_comb ct
+      in Thm.combination (Thm.reflexive ct1) (conv ct2) end
+  | _ => raise TERM ("Trueprop_conv", []));
 
 val conj = Const ("op &", [boolT, boolT] ---> boolT)
 and disj = Const ("op |", [boolT, boolT] ---> boolT)