changeset 15032 | 02aed07e01bf |
parent 14261 | 6c418d139f74 |
child 15616 | cdf6eeb4ac27 |
--- a/src/HOL/Auth/Public.thy Fri Jul 09 16:33:20 2004 +0200 +++ b/src/HOL/Auth/Public.thy Sun Jul 11 20:33:22 2004 +0200 @@ -435,7 +435,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" end