--- a/src/HOL/Auth/OtwayReesBella.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy Wed Nov 29 15:44:51 2006 +0100
@@ -142,9 +142,7 @@
*}
method_setup parts_explicit = {*
- Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- parts_explicit_tac 1)) *}
+ Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
"to explicitly state that some message components belong to parts knows Spy"
@@ -263,8 +261,8 @@
method_setup analz_freshCryptK = {*
Method.ctxt_args (fn ctxt =>
- (Method.METHOD
- (fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
+ (Method.SIMPLE_METHOD
+ (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac analz_image_freshCryptK_lemma),
ALLGOALS (asm_simp_tac (Simplifier.context ctxt analz_image_freshK_ss))]))) *}
"for proving useful rewrite rule"
@@ -272,8 +270,8 @@
method_setup disentangle = {*
Method.no_args
- (Method.METHOD
- (fn facts => REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
+ (Method.SIMPLE_METHOD
+ (REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
ORELSE' hyp_subst_tac))) *}
"for eliminating conjunctions, disjunctions and the like"