--- a/src/FOL/cladata.ML Sun Jul 30 13:01:09 2000 +0200
+++ b/src/FOL/cladata.ML Sun Jul 30 13:01:50 2000 +0200
@@ -33,7 +33,8 @@
structure Cla = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]);
+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!*)
--- a/src/HOL/cladata.ML Sun Jul 30 13:01:09 2000 +0200
+++ b/src/HOL/cladata.ML Sun Jul 30 13:01:50 2000 +0200
@@ -55,7 +55,8 @@
structure Classical = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
-structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
+structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
+ 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]