simplified BLAST_DATA;
authorwenzelm
Sat May 14 13:32:33 2011 +0200 (2011-05-14)
changeset 4280251d7e74f6899
parent 42801 da4ad5f98953
child 42803 7ed59879b1b6
simplified BLAST_DATA;
src/FOL/FOL.thy
src/HOL/HOL.thy
src/Provers/blast.ML
     1.1 --- a/src/FOL/FOL.thy	Sat May 14 13:26:55 2011 +0200
     1.2 +++ b/src/FOL/FOL.thy	Sat May 14 13:32:33 2011 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4    structure Blast = Blast
     1.5    (
     1.6      structure Classical = Cla
     1.7 -    val thy = @{theory}
     1.8 +    val Trueprop_const = dest_Const @{const Trueprop}
     1.9      val equality_name = @{const_name eq}
    1.10      val not_name = @{const_name Not}
    1.11      val notE = @{thm notE}
     2.1 --- a/src/HOL/HOL.thy	Sat May 14 13:26:55 2011 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat May 14 13:32:33 2011 +0200
     2.3 @@ -929,7 +929,7 @@
     2.4    structure Blast = Blast
     2.5    (
     2.6      structure Classical = Classical
     2.7 -    val thy = @{theory}
     2.8 +    val Trueprop_const = dest_Const @{const Trueprop}
     2.9      val equality_name = @{const_name HOL.eq}
    2.10      val not_name = @{const_name Not}
    2.11      val notE = @{thm notE}
     3.1 --- a/src/Provers/blast.ML	Sat May 14 13:26:55 2011 +0200
     3.2 +++ b/src/Provers/blast.ML	Sat May 14 13:32:33 2011 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4  signature BLAST_DATA =
     3.5  sig
     3.6    structure Classical: CLASSICAL
     3.7 -  val thy: theory
     3.8 +  val Trueprop_const: string * typ
     3.9    val equality_name: string
    3.10    val not_name: string
    3.11    val notE: thm           (* [| ~P;  P |] ==> R *)
    3.12 @@ -172,8 +172,7 @@
    3.13  fun isGoal (Const ("*Goal*", _) $ _) = true
    3.14    | isGoal _ = false;
    3.15  
    3.16 -val TruepropC = Object_Logic.judgment_name Data.thy;  (* FIXME *)
    3.17 -val TruepropT = Sign.the_const_type Data.thy TruepropC;
    3.18 +val (TruepropC, TruepropT) = Data.Trueprop_const;
    3.19  
    3.20  fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
    3.21