blast: cla_method';

--- a/src/FOL/cladata.ML	Wed Nov 18 11:02:42 1998 +0100
+++ b/src/FOL/cladata.ML	Wed Nov 18 11:03:49 1998 +0100
@@ -21,7 +21,8 @@
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
-open Cla;
+structure BasicClassical: BASIC_CLASSICAL = Cla;
+open BasicClassical;
 
 (*Better for fast_tac: needs no quantifier duplication!*)
 qed_goal "alt_ex1E" IFOL.thy
@@ -57,11 +58,10 @@
   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'
   end;
 
 structure Blast = BlastFun(Blast_Data);
 
 val Blast_tac = Blast.Blast_tac
 and blast_tac = Blast.blast_tac;
-
-

--- a/src/HOL/cladata.ML	Wed Nov 18 11:02:42 1998 +0100
+++ b/src/HOL/cladata.ML	Wed Nov 18 11:03:49 1998 +0100
@@ -76,6 +76,7 @@
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
   val claset	= Classical.claset
   val rep_cs    = Classical.rep_cs
+  val cla_method' = Classical.cla_method'
   end;
 
 structure Blast = BlastFun(Blast_Data);