src/FOL/cladata.ML
changeset 7355 4c43090659ca
parent 7156 3e84e73a3b6a
child 8099 6a087be9f6d9
--- a/src/FOL/cladata.ML	Wed Aug 25 20:42:01 1999 +0200
+++ b/src/FOL/cladata.ML	Wed Aug 25 20:45:19 1999 +0200
@@ -3,10 +3,9 @@
     Author:     Tobias Nipkow
     Copyright   1996  University of Cambridge
 
-Setting up the classical reasoner 
+Setting up the classical reasoner.
 *)
 
-
 section "Classical Reasoner";
 
 
@@ -24,6 +23,7 @@
 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);                                              \
@@ -44,25 +44,4 @@
 val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
                      addSEs [exE,alt_ex1E] addEs [allE];
 
-claset_ref() := FOL_cs;
-
-
-(*** Applying BlastFun to create Blast_tac ***)
-structure Blast_Data = 
-  struct
-  type claset	= Cla.claset
-  val notE	= notE
-  val ccontr	= ccontr
-  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_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 clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)];