diff -r 1fb807260ff1 -r a092ae7bb2a6 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Fri Nov 03 21:29:56 2000 +0100
+++ b/src/FOL/cladata.ML	Fri Nov 03 21:31:11 2000 +0100
@@ -24,12 +24,11 @@
   val classical = classical
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
+  val atomize	= thms "atomize"
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-structure Obtain = ObtainFun(val atomic_thesis = FOLogic.atomic_Trueprop and
-  that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
 
 
 (*Better for fast_tac: needs no quantifier duplication!*)