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