--- a/src/HOL/SET_Protocol/Message_SET.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy Thu Apr 18 17:07:01 2013 +0200
@@ -853,12 +853,12 @@
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));
@@ -871,7 +871,7 @@
(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);
*}
@@ -932,7 +932,7 @@
"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