src/FOL/blastdata.ML
changeset 7355 4c43090659ca
child 9486 2df511ebb956
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/blastdata.ML	Wed Aug 25 20:45:19 1999 +0200
@@ -0,0 +1,20 @@
+
+(*** 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 hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
+  val claset	= Cla.claset
+  val rep_cs    = Cla.rep_cs
+  val cla_modifiers = Cla.cla_modifiers;
+  val cla_meth' = Cla.cla_meth'
+  end;
+
+structure Blast = BlastFun(Blast_Data);
+
+val Blast_tac = Blast.Blast_tac
+and blast_tac = Blast.blast_tac;