diff -r dcfab8e87621 -r f2e92fc0c8aa src/Provers/clasimp.ML
--- 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*)