src/Provers/clasimp.ML

 structure Blast = Data.Blast;
 
 
 (* simp as classical wrapper *)
 
-fun clasimp f name tac ctxt = f (ctxt, (name, CHANGED o tac (simpset_of ctxt)));
+(* FIXME !? *)
+fun clasimp f name tac ctxt = f (ctxt, (name, fn _ => CHANGED o tac ctxt));
 
 (*Add a simpset to the claset!*)
 (*Caution: only one simpset added can be added by each of addSss and addss*)
 val addSss = clasimp Classical.addSafter "safe_asm_full_simp_tac" Simplifier.safe_asm_full_simp_tac;
 val addss = clasimp Classical.addbefore "asm_full_simp_tac" Simplifier.asm_full_simp_tac;

 
 
 (* tactics *)
 
 fun clarsimp_tac ctxt =
-  Simplifier.safe_asm_full_simp_tac (simpset_of ctxt) THEN_ALL_NEW
+  Simplifier.safe_asm_full_simp_tac ctxt THEN_ALL_NEW
   Classical.clarify_tac (addSss ctxt);
 
 
 (* auto_tac *)
 

     val main_tac =
       Blast.depth_tac ctxt m  (* fast but can't use wrappers *)
       ORELSE'
       (CHANGED o nodup_depth_tac (addss ctxt) n);  (* slower but more general *)
   in
-    PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac (simpset_of ctxt))) THEN
+    PARALLEL_GOALS (ALLGOALS (Simplifier.asm_full_simp_tac ctxt)) THEN
     TRY (Classical.safe_tac ctxt) THEN
     REPEAT_DETERM (FIRSTGOAL main_tac) THEN
     TRY (Classical.safe_tac (addSss ctxt)) THEN
     prune_params_tac
   end;

 (* aimed to solve the given subgoal totally, using whatever tools possible *)
 fun force_tac ctxt =
   let val ctxt' = addss ctxt in
     SELECT_GOAL
      (Classical.clarify_tac ctxt' 1 THEN
-      IF_UNSOLVED (Simplifier.asm_full_simp_tac (simpset_of ctxt) 1) THEN
+      IF_UNSOLVED (Simplifier.asm_full_simp_tac ctxt 1) THEN
       ALLGOALS (Classical.first_best_tac ctxt'))
   end;
 
 
 (* basic combinations *)