changeset 51703 | f2e92fc0c8aa |
parent 50111 | 9e04e6edc5e7 |
child 51717 | 9e7d1c139569 |
--- a/src/Provers/clasimp.ML Fri Apr 12 17:02:55 2013 +0200 +++ b/src/Provers/clasimp.ML Fri Apr 12 17:21:51 2013 +0200 @@ -44,8 +44,7 @@ (* simp as classical wrapper *) -fun clasimp f name tac ctxt = - Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt; +fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt))); (*Add a simpset to the claset!*) (*Caution: only one simpset added can be added by each of addSss and addss*)