clasimp: include Splitter;
authorwenzelm
Wed, 15 Mar 2000 18:42:54 +0100
changeset 8472 50a653f8b8ea
parent 8471 36446bf42b16
child 8473 2798d2f71ec2
clasimp: include Splitter;
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);