src/HOL/SET_Protocol/Message_SET.thy

 val Fake_insert_tac =
     dresolve_tac [impOfSubs @{thm Fake_analz_insert},
                   impOfSubs @{thm Fake_parts_insert}] THEN'
     eresolve_tac [asm_rl, @{thm synth.Inj}];
 
-fun Fake_insert_simp_tac ss i =
-  REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ss i;
+fun Fake_insert_simp_tac ctxt i =
+  REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ctxt i;
 
 fun atomic_spy_analz_tac ctxt =
   SELECT_GOAL
-    (Fake_insert_simp_tac (simpset_of ctxt) 1 THEN
+    (Fake_insert_simp_tac ctxt 1 THEN
       IF_UNSOLVED
         (Blast.depth_tac (ctxt addIs [@{thm analz_insertI},
             impOfSubs @{thm analz_subset_parts}]) 4 1));
 
 fun spy_analz_tac ctxt i =

      (EVERY
       [  (*push in occurrences of X...*)
        (REPEAT o CHANGED)
            (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1),
        (*...allowing further simplifications*)
-       simp_tac (simpset_of ctxt) 1,
+       simp_tac ctxt 1,
        REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])),
        DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i);
 *}
 (*>*)
 

 method_setup atomic_spy_analz = {*
     Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac) *}
     "for debugging spy_analz"
 
 method_setup Fake_insert_simp = {*
-    Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *}
+    Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac) *}
     "for debugging spy_analz"
 
 end