diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Fri Jul 09 16:33:20 2004 +0200 +++ b/src/HOL/SET-Protocol/PublicSET.thy Sun Jul 11 20:33:22 2004 +0200 @@ -374,7 +374,7 @@ method_setup possibility = {* Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => - gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} + gen_possibility_tac (local_simpset_of ctxt))) *} "for proving possibility theorems"