# HG changeset patch
# User wenzelm
# Date 953142174 -3600
# Node ID 50a653f8b8ea0ddd27b9eba7f1a353b724f3b8a2
# Parent  36446bf42b16a76a7ebec366c156e7510e0a0be9
clasimp: include Splitter;

diff -r 36446bf42b16 -r 50a653f8b8ea src/FOL/simpdata.ML
--- 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);