| changeset 18529 | 540da2415751 |
| parent 18324 | d1c4b1112e33 |
| child 18708 | 4b3dadb4fe33 |
--- a/src/FOL/simpdata.ML Sat Dec 31 21:49:35 2005 +0100 +++ b/src/FOL/simpdata.ML Sat Dec 31 21:49:36 2005 +0100 @@ -369,8 +369,7 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter and Classical = Cla and Blast = Blast - val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE - val cla_make_elim = cla_make_elim); + val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE); open Clasimp; val FOL_css = (FOL_cs, FOL_ss);