--- a/src/HOL/HOL.thy Wed Mar 15 18:42:54 2000 +0100
+++ b/src/HOL/HOL.thy Wed Mar 15 18:47:28 2000 +0100
@@ -188,7 +188,9 @@
use "HOL_lemmas.ML" setup attrib_setup
use "cladata.ML" setup Classical.setup setup clasetup
use "blastdata.ML" setup Blast.setup
-use "simpdata.ML" setup Simplifier.setup setup iff_attrib_setup
+use "simpdata.ML" setup Simplifier.setup
+ setup "Simplifier.method_setup Splitter.split_modifiers"
+ setup Splitter.setup setup iff_attrib_setup
setup simpsetup setup Clasimp.setup
--- a/src/HOL/simpdata.ML Wed Mar 15 18:42:54 2000 +0100
+++ b/src/HOL/simpdata.ML Wed Mar 15 18:47:28 2000 +0100
@@ -517,9 +517,8 @@
(*** integration of simplifier with classical reasoner ***)
structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier
- and Classical = Classical
- and Blast = Blast);
+ (structure Simplifier = Simplifier and Splitter = Splitter
+ and Classical = Classical and Blast = Blast);
open Clasimp;
val HOL_css = (HOL_cs, HOL_ss);