# HG changeset patch
# User wenzelm
# Date 933610226 -7200
# Node ID 3e84e73a3b6a7382df87dcfbd9f7d1bd0cb8a4e0
# Parent  70ba7d640bfec4724e9a8babf4ad464786989f65
fixed Blast_Data;

diff -r 70ba7d640bfe -r 3e84e73a3b6a src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Mon Aug 02 17:59:25 1999 +0200
+++ b/src/FOL/cladata.ML	Mon Aug 02 18:10:26 1999 +0200
@@ -58,7 +58,8 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Cla.claset
   val rep_cs    = Cla.rep_cs
-  val cla_method' = Cla.cla_method'
+  val cla_modifiers = Cla.cla_modifiers;
+  val cla_meth' = Cla.cla_meth'
   end;
 
 structure Blast = BlastFun(Blast_Data);