--- a/src/HOL/Hyperreal/HyperDef.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Sun Jul 11 20:33:22 2004 +0200
@@ -208,15 +208,13 @@
method_setup fuf = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- fuf_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ fuf_tac (local_clasimpset_of ctxt) 1)) *}
"free ultrafilter tactic"
method_setup ultra = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- ultra_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ ultra_tac (local_clasimpset_of ctxt) 1)) *}
"ultrafilter tactic"