src/HOL/Deriv.thy
changeset 31902 862ae16a799d
parent 31899 1a7ade46061b
child 33654 abf780db30ea
--- 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