changeset 30549 | d2d7874648bd |
parent 30510 | 4120fc59dd85 |
child 30607 | c3d1590debd8 |
--- a/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 17:51:24 2009 +0100 +++ b/src/HOL/SET-Protocol/PublicSET.thy Mon Mar 16 18:24:30 2009 +0100 @@ -371,7 +371,7 @@ *} method_setup possibility = {* - Method.ctxt_args (fn ctxt => + Scan.succeed (fn ctxt => SIMPLE_METHOD (PublicSET.gen_possibility_tac (local_simpset_of ctxt))) *} "for proving possibility theorems"