# HG changeset patch
# User wenzelm
# Date 1246548816 -7200
# Node ID e280491f36b8dda11b040012ee0d7b754f6bd03c
# Parent  7c35d9ad0349037165630442962711becd63bccf
renamed NamedThmsFun to Named_Thms;

diff -r 7c35d9ad0349 -r e280491f36b8 NEWS
--- a/NEWS	Thu Jul 02 17:30:54 2009 +0200
+++ b/NEWS	Thu Jul 02 17:33:36 2009 +0200
@@ -80,7 +80,7 @@
 boundaries of intervals and implements interval splitting and Taylor
 series expansion.
 
-* Changed DERIV_intros to a dynamic fact (via NamedThmsFun).  Each of
+* Changed DERIV_intros to a dynamic fact (via Named_Thms).  Each of
 the theorems in DERIV_intros assumes composition with an additional
 function and matches a variable to the derivative, which has to be
 solved by the simplifier.  Hence (auto intro!: DERIV_intros) computes
@@ -92,6 +92,8 @@
 
 *** ML ***
 
+* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
+
 * Eliminated old Attrib.add_attributes, Method.add_methods and related
 cominators for "args".  INCOMPATIBILITY, need to use simplified
 Attrib/Method.setup introduced in Isabelle2009.
diff -r 7c35d9ad0349 -r e280491f36b8 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Thu Jul 02 17:30:54 2009 +0200
+++ b/src/Pure/Tools/named_thms.ML	Thu Jul 02 17:33:36 2009 +0200
@@ -14,7 +14,7 @@
   val setup: theory -> theory
 end;
 
-functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
+functor Named_Thms(val name: string val description: string): NAMED_THMS =
 struct
 
 structure Data = GenericDataFun