# HG changeset patch
# User wenzelm
# Date 1305372753 -7200
# Node ID 51d7e74f6899c0b5fbe6df12903ba11ff917e561
# Parent  da4ad5f989532907cee9f325195be5dabc74ec8f
simplified BLAST_DATA;

diff -r da4ad5f98953 -r 51d7e74f6899 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat May 14 13:26:55 2011 +0200
+++ b/src/FOL/FOL.thy	Sat May 14 13:32:33 2011 +0200
@@ -201,7 +201,7 @@
   structure Blast = Blast
   (
     structure Classical = Cla
-    val thy = @{theory}
+    val Trueprop_const = dest_Const @{const Trueprop}
     val equality_name = @{const_name eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
diff -r da4ad5f98953 -r 51d7e74f6899 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 14 13:26:55 2011 +0200
+++ b/src/HOL/HOL.thy	Sat May 14 13:32:33 2011 +0200
@@ -929,7 +929,7 @@
   structure Blast = Blast
   (
     structure Classical = Classical
-    val thy = @{theory}
+    val Trueprop_const = dest_Const @{const Trueprop}
     val equality_name = @{const_name HOL.eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
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);