--- a/src/FOL/IFOL.thy Mon Nov 03 12:24:13 1997 +0100 +++ b/src/FOL/IFOL.thy Mon Nov 03 12:26:45 1997 +0100 @@ -112,3 +112,6 @@ iff_reflection "(P<->Q) ==> (P==Q)" end + + +ML val thy_data = [Simplifier.simpset_thy_data];