# HG changeset patch
# User wenzelm
# Date 911383429 -3600
# Node ID 890f2f9b926df897e0c6402e41325f6f94105c19
# Parent  6e00a206a94869f443c4bb6ec06b5adf5fb367d8
blast: cla_method';

diff -r 6e00a206a948 -r 890f2f9b926d src/FOL/cladata.ML
--- 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;
-
-
diff -r 6e00a206a948 -r 890f2f9b926d src/HOL/cladata.ML
--- 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);