diff -r 5a3e5e46d977 -r 184d7601c062 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 17:54:36 2008 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Jun 16 17:54:38 2008 +0200
@@ -48,13 +48,12 @@
 
 in
 
-val deriv_tac =
-  SUBGOAL (fn (prem,i) =>
-   (resolve_tac @{thms deriv_rulesI} i) ORELSE
-    ((rtac (Drule.read_instantiate [("f",get_fun_name prem)]
-                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
+fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
+  resolve_tac @{thms deriv_rulesI} i ORELSE
+    ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)]
+                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
 
-val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
+fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
 
 end
 *}
@@ -71,8 +70,8 @@
 apply clarify
 apply (rule DERIV_diff)
 apply (simp (no_asm_simp))
-apply (tactic DERIV_tac)
-apply (tactic DERIV_tac)
+apply (tactic {* DERIV_tac @{context} *})
+apply (tactic {* DERIV_tac @{context} *})
 apply (rule_tac [2] lemma_DERIV_subst)
 apply (rule_tac [2] DERIV_quotient)
 apply (rule_tac [3] DERIV_const)