diff -r a7ee88ef2fa5 -r 6a087be9f6d9 src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Jan 05 11:50:13 2000 +0100
+++ b/src/FOL/cladata.ML	Wed Jan 05 11:50:55 2000 +0100
@@ -20,8 +20,8 @@
   end;
 
 structure Cla = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Cla;
-open BasicClassical;
+structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
+structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
 
 
 (*Better for fast_tac: needs no quantifier duplication!*)