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