# HG changeset patch
# User wenzelm
# Date 964954910 -7200
# Node ID b63b21f370ca8b8bea6d661196068b94274aaeec
# Parent  f778551af3edd613e3f61a1c68b2f7fd46c07802
updated ObtainFun;

diff -r f778551af3ed -r b63b21f370ca src/FOL/cladata.ML
--- 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!*)
diff -r f778551af3ed -r b63b21f370ca src/HOL/cladata.ML
--- 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]