--- 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);