| changeset 15032 | 02aed07e01bf |
| parent 14218 | db95d1c2f51b |
| child 16417 | 9bc16273c2d4 |
--- 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"