src/FOL/cladata.ML

   val classical = classical
   val hyp_subst_tacs=[hyp_subst_tac]
   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
     "[| EX! x. P(x);                                              \
 \       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \

   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_method' = Cla.cla_method'
   end;
 
 structure Blast = BlastFun(Blast_Data);
 
 val Blast_tac = Blast.Blast_tac
 and blast_tac = Blast.blast_tac;
-
-