diff -r da4ad5f98953 -r 51d7e74f6899 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat May 14 13:26:55 2011 +0200
+++ b/src/Provers/blast.ML	Sat May 14 13:32:33 2011 +0200
@@ -41,7 +41,7 @@
 signature BLAST_DATA =
 sig
   structure Classical: CLASSICAL
-  val thy: theory
+  val Trueprop_const: string * typ
   val equality_name: string
   val not_name: string
   val notE: thm           (* [| ~P;  P |] ==> R *)
@@ -172,8 +172,7 @@
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = Object_Logic.judgment_name Data.thy;  (* FIXME *)
-val TruepropT = Sign.the_const_type Data.thy TruepropC;
+val (TruepropC, TruepropT) = Data.Trueprop_const;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);