# HG changeset patch
# User wenzelm
# Date 947069455 -3600
# Node ID 6a087be9f6d9cde6fc270e523a924070f1ef6f54
# Parent  a7ee88ef2fa53e2551bed12c92426edcac9cb7cd
ObtainFun;

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!*)
diff -r a7ee88ef2fa5 -r 6a087be9f6d9 src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Wed Jan 05 11:50:13 2000 +0100
+++ b/src/HOL/cladata.ML	Wed Jan 05 11:50:55 2000 +0100
@@ -40,8 +40,8 @@
   end;
 
 structure Classical = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Classical;
-open BasicClassical;
+structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
+structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
 
 (*Propositional rules*)
 val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]