simplified Blast setup;

--- a/src/FOL/FOL.thy	Tue Apr 26 21:05:52 2011 +0200
+++ b/src/FOL/FOL.thy	Tue Apr 26 21:27:01 2011 +0200
@@ -174,18 +174,13 @@
 ML {*
   structure Blast = Blast
   (
+    structure Classical = Cla
     val thy = @{theory}
-    type claset = Cla.claset
     val equality_name = @{const_name eq}
     val not_name = @{const_name Not}
     val notE = @{thm notE}
     val ccontr = @{thm ccontr}
-    val contr_tac = Cla.contr_tac
-    val dup_intr = Cla.dup_intr
     val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
-    val rep_cs = Cla.rep_cs
-    val cla_modifiers = Cla.cla_modifiers
-    val cla_meth' = Cla.cla_meth'
   );
   val blast_tac = Blast.blast_tac;
 *}

--- a/src/HOL/HOL.thy	Tue Apr 26 21:05:52 2011 +0200
+++ b/src/HOL/HOL.thy	Tue Apr 26 21:27:01 2011 +0200
@@ -927,22 +927,17 @@
 done
 
 ML {*
-structure Blast = Blast
-(
-  val thy = @{theory}
-  type claset = Classical.claset
-  val equality_name = @{const_name HOL.eq}
-  val not_name = @{const_name Not}
-  val notE = @{thm notE}
-  val ccontr = @{thm ccontr}
-  val contr_tac = Classical.contr_tac
-  val dup_intr = Classical.dup_intr
-  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
-  val rep_cs = Classical.rep_cs
-  val cla_modifiers = Classical.cla_modifiers
-  val cla_meth' = Classical.cla_meth'
-);
-val blast_tac = Blast.blast_tac;
+  structure Blast = Blast
+  (
+    structure Classical = Classical
+    val thy = @{theory}
+    val equality_name = @{const_name HOL.eq}
+    val not_name = @{const_name Not}
+    val notE = @{thm notE}
+    val ccontr = @{thm ccontr}
+    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+  );
+  val blast_tac = Blast.blast_tac;
 *}
 
 setup Blast.setup

--- a/src/Provers/blast.ML	Tue Apr 26 21:05:52 2011 +0200
+++ b/src/Provers/blast.ML	Tue Apr 26 21:27:01 2011 +0200
@@ -40,24 +40,13 @@
 
 signature BLAST_DATA =
 sig
+  structure Classical: CLASSICAL
   val thy: theory
-  type claset
   val equality_name: string
   val not_name: string
-  val notE              : thm           (* [| ~P;  P |] ==> R *)
-  val ccontr            : thm
-  val contr_tac         : int -> tactic
-  val dup_intr          : thm -> thm
-  val hyp_subst_tac     : bool -> int -> tactic
-  val rep_cs    : (* dependent on classical.ML *)
-      claset -> {safeIs: thm list, safeEs: thm list,
-                 hazIs: thm list, hazEs: thm list,
-                 swrappers: (string * wrapper) list,
-                 uwrappers: (string * wrapper) list,
-                 safe0_netpair: netpair, safep_netpair: netpair,
-                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
-  val cla_modifiers: Method.modifier parser list
-  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
+  val notE: thm           (* [| ~P;  P |] ==> R *)
+  val ccontr: thm
+  val hyp_subst_tac: bool -> int -> tactic
 end;
 
 signature BLAST =
@@ -72,31 +61,31 @@
     | Bound of int
     | Abs   of string*term
     | $  of term*term;
-  type branch
-  val depth_tac         : claset -> int -> int -> tactic
-  val depth_limit       : int Config.T
-  val blast_tac         : claset -> int -> tactic
-  val setup             : theory -> theory
+  val depth_tac: claset -> int -> int -> tactic
+  val depth_limit: int Config.T
+  val blast_tac: claset -> int -> tactic
+  val setup: theory -> theory
   (*debugging tools*)
-  val stats             : bool Unsynchronized.ref
-  val trace             : bool Unsynchronized.ref
-  val fullTrace         : branch list list Unsynchronized.ref
-  val fromType          : (indexname * term) list Unsynchronized.ref -> Term.typ -> term
-  val fromTerm          : theory -> Term.term -> term
-  val fromSubgoal       : theory -> Term.term -> term
-  val instVars          : term -> (unit -> unit)
-  val toTerm            : int -> term -> Term.term
-  val readGoal          : theory -> string -> term
-  val tryInThy          : theory -> claset -> int -> string ->
-                  (int->tactic) list * branch list list * (int*int*exn) list
-  val normBr            : branch -> branch
+  type branch
+  val stats: bool Unsynchronized.ref
+  val trace: bool Unsynchronized.ref
+  val fullTrace: branch list list Unsynchronized.ref
+  val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term
+  val fromTerm: theory -> Term.term -> term
+  val fromSubgoal: theory -> Term.term -> term
+  val instVars: term -> (unit -> unit)
+  val toTerm: int -> term -> Term.term
+  val readGoal: theory -> string -> term
+  val tryInThy: theory -> claset -> int -> string ->
+    (int -> tactic) list * branch list list * (int * int * exn) list
+  val normBr: branch -> branch
 end;
 
-
-functor Blast(Data: BLAST_DATA) : BLAST =
+functor Blast(Data: BLAST_DATA): BLAST =
 struct
 
-type claset = Data.claset;
+structure Classical = Data.Classical;
+type claset = Classical.claset;
 
 val trace = Unsynchronized.ref false
 and stats = Unsynchronized.ref false;   (*for runtime and search statistics*)
@@ -541,7 +530,7 @@
 fun fromIntrRule thy vars rl =
   let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars
       fun tac (upd,dup,rot) i =
-         rmtac upd (if dup then Data.dup_intr rl else rl) i
+         rmtac upd (if dup then Classical.dup_intr rl else rl) i
          THEN
          rot_subgoals_tac (rot, #2 trl) i
   in (trl, tac) end;
@@ -928,7 +917,7 @@
 *)
 fun prove (state, start, cs, brs, cont) =
  let val State {thy, ntrail, nclosed, ntried, ...} = state;
-     val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
+     val {safe0_netpair, safep_netpair, haz_netpair, ...} = Classical.rep_cs cs
      val safeList = [safe0_netpair, safep_netpair]
      and hazList  = [haz_netpair]
      fun prv (tacs, trs, choices, []) =
@@ -1314,9 +1303,9 @@
 val setup =
   setup_depth_limit #>
   Method.setup @{binding blast}
-    (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
-      (fn NONE => Data.cla_meth' blast_tac
-        | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
+    (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
+      (fn NONE => Classical.cla_meth' blast_tac
+        | SOME lim => Classical.cla_meth' (fn cs => depth_tac cs lim)))
     "classical tableau prover";
 
 end;