diff -r d9805c5b5d2e -r 983e8b6e4e69 src/FOL/blastdata.ML
--- a/src/FOL/blastdata.ML	Fri Mar 20 17:04:44 2009 +0100
+++ b/src/FOL/blastdata.ML	Fri Mar 20 17:12:37 2009 +0100
@@ -1,5 +1,5 @@
 
-(*** Applying BlastFun to create Blast_tac ***)
+(*** Applying BlastFun to create blast_tac ***)
 structure Blast_Data = 
   struct
   type claset	= Cla.claset
@@ -10,13 +10,10 @@
   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 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;
+val blast_tac = Blast.blast_tac;