src/HOL/Deriv.thy

--- a/src/HOL/Deriv.thy	Thu Jul 02 17:33:36 2009 +0200
+++ b/src/HOL/Deriv.thy	Thu Jul 02 17:34:14 2009 +0200
@@ -315,14 +315,14 @@
 
 text {* @{text "DERIV_intros"} *}
 ML {*
-structure DerivIntros = NamedThmsFun
+structure Deriv_Intros = Named_Thms
 (
   val name = "DERIV_intros"
   val description = "DERIV introduction rules"
 )
 *}
 
-setup DerivIntros.setup
+setup Deriv_Intros.setup
 
 lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
   by simp