diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -31,18 +31,24 @@
 text{*A crude tactic to differentiate by proof.*}
 ML
 {*
+local
+val deriv_rulesI =
+  [thm "DERIV_Id", 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_Id", 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;
 
-val deriv_rulesI = [DERIV_Id,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_Id,DERIV_const,DERIV_cos];
-
 val deriv_tac =
   SUBGOAL (fn (prem,i) =>
    (resolve_tac deriv_rulesI i) ORELSE
@@ -50,6 +56,8 @@
                      DERIV_chain2) i) handle DERIV_name => no_tac));;
 
 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
+
+end
 *}
 
 lemma Maclaurin_lemma2: