| changeset 18529 | 540da2415751 |
| parent 18407 | fa075b606571 |
| child 18708 | 4b3dadb4fe33 |
--- a/src/HOL/simpdata.ML Sat Dec 31 21:49:35 2005 +0100 +++ b/src/HOL/simpdata.ML Sat Dec 31 21:49:36 2005 +0100 @@ -433,8 +433,7 @@ structure Clasimp = ClasimpFun (structure Simplifier = Simplifier and Splitter = Splitter and Classical = Classical 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 HOL_css = (HOL_cs, HOL_ss);