src/HOL/Hyperreal/MacLaurin.thy

--- a/src/HOL/Hyperreal/MacLaurin.thy	Wed Jun 11 18:01:36 2008 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Wed Jun 11 18:02:00 2008 +0200
@@ -51,7 +51,7 @@
 val deriv_tac =
   SUBGOAL (fn (prem,i) =>
    (resolve_tac @{thms deriv_rulesI} i) ORELSE
-    ((rtac (read_instantiate [("f",get_fun_name prem)]
+    ((rtac (Drule.read_instantiate [("f",get_fun_name prem)]
                      @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
 
 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));