src/HOL/simpdata.ML

--- 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);