src/FOL/simpdata.ML
changeset 8472 50a653f8b8ea
parent 7570 a9391550eea1
child 8643 331f0c75e3dc
--- a/src/FOL/simpdata.ML	Wed Mar 15 18:42:13 2000 +0100
+++ b/src/FOL/simpdata.ML	Wed Mar 15 18:42:54 2000 +0100
@@ -355,9 +355,8 @@
 (*** integration of simplifier with classical reasoner ***)
 
 structure Clasimp = ClasimpFun
- (structure Simplifier = Simplifier 
-        and Classical  = Cla
-        and Blast      = Blast);
+ (structure Simplifier = Simplifier and Splitter = Splitter
+   and Classical  = Cla and Blast = Blast);
 open Clasimp;
 
 val FOL_css = (FOL_cs, FOL_ss);