# HG changeset patch
# User paulson
# Date 859987180 -7200
# Node ID 0aa5a3cd45507526f098af8ee7b854478a972a64
# Parent  0a648ebbf6d4dca4d5022d5ec03bb33b2662174e
Now builds blast_tac

diff -r 0a648ebbf6d4 -r 0aa5a3cd4550 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Apr 02 15:18:21 1997 +0200
+++ b/src/FOL/cladata.ML	Wed Apr 02 15:19:40 1997 +0200
@@ -7,7 +7,6 @@
 *)
 
 
-(** Applying HypsubstFun to generate hyp_subst_tac **)
 section "Classical Reasoner";
 
 
@@ -62,3 +61,22 @@
 
 claset := FOL_cs;
 
+(*** Applying BlastFun to create Blast_tac ***)
+structure Blast_Data = 
+  struct
+  type claset	= Cla.claset
+  val notE	= notE
+  val ccontr	= ccontr
+  val contr_tac = Cla.contr_tac
+  val dup_intr	= Cla.dup_intr
+  val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac
+  val claset	= Cla.claset
+  val rep_claset = Cla.rep_claset
+  end;
+
+structure Blast = BlastFun(Blast_Data);
+
+val Blast_tac = Blast.Blast_tac
+and blast_tac = Blast.blast_tac;
+
+