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