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