diff -r c89d77d97f84 -r 9f818139951b src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 07 20:43:36 2007 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Tue Aug 07 23:24:10 2007 +0200
@@ -29,31 +29,30 @@
 by arith
 
 text{*A crude tactic to differentiate by proof.*}
+
+lemmas deriv_rulesI =
+  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
+  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
+  DERIV_add DERIV_diff DERIV_mult DERIV_minus
+  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
+  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
+  DERIV_ident DERIV_const DERIV_cos
+
 ML
 {*
 local
-val deriv_rulesI =
-  [thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
-  thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
-  thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
-  thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
-  thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
-  thm "DERIV_ident", thm "DERIV_const", thm "DERIV_cos"];
-
-val DERIV_chain2 = thm "DERIV_chain2";
-
-in
-
 exception DERIV_name;
 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
 |   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
 |   get_fun_name _ = raise DERIV_name;
 
+in
+
 val deriv_tac =
   SUBGOAL (fn (prem,i) =>
-   (resolve_tac deriv_rulesI i) ORELSE
+   (resolve_tac @{thms deriv_rulesI} i) ORELSE
     ((rtac (read_instantiate [("f",get_fun_name prem)]
-                     DERIV_chain2) i) handle DERIV_name => no_tac));;
+                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));;
 
 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));