diff -r f06fc940c61c -r 36446bf42b16 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Mar 15 18:41:00 2000 +0100
+++ b/src/FOL/FOL.thy	Wed Mar 15 18:42:13 2000 +0100
@@ -6,9 +6,11 @@
   classical: "(~P ==> P) ==> P"
 
 use "FOL_lemmas1.ML"
-use "cladata.ML"	setup Cla.setup setup clasetup
-use "blastdata.ML"	setup Blast.setup
+use "cladata.ML"        setup Cla.setup setup clasetup
+use "blastdata.ML"      setup Blast.setup
 use "FOL_lemmas2.ML"
-use "simpdata.ML"	setup simpsetup setup Clasimp.setup
+use "simpdata.ML"       setup simpsetup
+                        setup "Simplifier.method_setup Splitter.split_modifiers"
+                        setup Splitter.setup setup Clasimp.setup
 
 end