src/Provers/blast.ML
changeset 32176 893614e2c35c
parent 32174 9036cc8ae775
child 32740 9dd0a2f83429
     1.1 --- a/src/Provers/blast.ML	Fri Jul 24 21:18:05 2009 +0200
     1.2 +++ b/src/Provers/blast.ML	Fri Jul 24 21:21:45 2009 +0200
     1.3 @@ -39,7 +39,8 @@
     1.4  type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
     1.5  
     1.6  signature BLAST_DATA =
     1.7 -  sig
     1.8 +sig
     1.9 +  val thy: theory
    1.10    type claset
    1.11    val equality_name: string
    1.12    val not_name: string
    1.13 @@ -57,11 +58,10 @@
    1.14                   haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
    1.15    val cla_modifiers: Method.modifier parser list
    1.16    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    1.17 -  end;
    1.18 -
    1.19 +end;
    1.20  
    1.21  signature BLAST =
    1.22 -  sig
    1.23 +sig
    1.24    type claset
    1.25    exception TRANS of string    (*reports translation errors*)
    1.26    datatype term =
    1.27 @@ -90,10 +90,10 @@
    1.28    val tryInThy          : theory -> claset -> int -> string ->
    1.29                    (int->tactic) list * branch list list * (int*int*exn) list
    1.30    val normBr            : branch -> branch
    1.31 -  end;
    1.32 +end;
    1.33  
    1.34  
    1.35 -functor BlastFun(Data: BLAST_DATA) : BLAST =
    1.36 +functor Blast(Data: BLAST_DATA) : BLAST =
    1.37  struct
    1.38  
    1.39  type claset = Data.claset;
    1.40 @@ -181,8 +181,8 @@
    1.41  fun isGoal (Const ("*Goal*", _) $ _) = true
    1.42    | isGoal _ = false;
    1.43  
    1.44 -val TruepropC = ObjectLogic.judgment_name (OldGoals.the_context ());
    1.45 -val TruepropT = Sign.the_const_type (OldGoals.the_context ()) TruepropC;
    1.46 +val TruepropC = ObjectLogic.judgment_name Data.thy;
    1.47 +val TruepropT = Sign.the_const_type Data.thy TruepropC;
    1.48  
    1.49  fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
    1.50