doc-src/TutorialI/Protocol/Public.thy

      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]));
 *}
 
-method_setup possibility = {* Method.no_args (SIMPLE_METHOD possibility_tac) *}
+method_setup possibility = {* Scan.succeed (K (SIMPLE_METHOD possibility_tac)) *}
     "for proving possibility theorems"
 
 end
 (*>*)