diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Hyperreal/HyperDef.thy
--- 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"