--- a/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy Fri Mar 13 19:58:26 2009 +0100
@@ -137,7 +137,7 @@
*}
method_setup parts_explicit = {*
- Method.no_args (Method.SIMPLE_METHOD' parts_explicit_tac) *}
+ Method.no_args (SIMPLE_METHOD' parts_explicit_tac) *}
"to explicitly state that some message components belong to parts knows Spy"
@@ -258,7 +258,7 @@
method_setup analz_freshCryptK = {*
Method.ctxt_args (fn ctxt =>
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
ALLGOALS (asm_simp_tac
@@ -268,7 +268,7 @@
method_setup disentangle = {*
Method.no_args
- (Method.SIMPLE_METHOD
+ (SIMPLE_METHOD
(REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE]
ORELSE' hyp_subst_tac))) *}
"for eliminating conjunctions, disjunctions and the like"