--- a/src/HOL/Hyperreal/HyperDef.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy Wed Nov 29 15:44:51 2006 +0100
@@ -183,14 +183,12 @@
method_setup fuf = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- fuf_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD' (fuf_tac (local_clasimpset_of ctxt))) *}
"free ultrafilter tactic"
method_setup ultra = {*
Method.ctxt_args (fn ctxt =>
- Method.METHOD (fn facts =>
- ultra_tac (local_clasimpset_of ctxt) 1)) *}
+ Method.SIMPLE_METHOD' (ultra_tac (local_clasimpset_of ctxt))) *}
"ultrafilter tactic"