# HG changeset patch
# User wenzelm
# Date 1119026022 -7200
# Node ID e0f22edf38a58287ae524959865f59603a16d3f7
# Parent  451f1c46d4ca9a2a872bf8bc6c9e51d747029791
Context.names_of;

diff -r 451f1c46d4ca -r e0f22edf38a5 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Jun 17 18:33:41 2005 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Fri Jun 17 18:33:42 2005 +0200
@@ -156,7 +156,7 @@
 
   (*Forbid the inductive definition structure from clashing with a theory
     name.  This restriction may become obsolete as ML is de-emphasized.*)
-  val dummy = deny (big_rec_base_name mem (Sign.stamp_names_of sign))
+  val dummy = deny (big_rec_base_name mem (Context.names_of sign))
                ("Definition " ^ big_rec_base_name ^
                 " would clash with the theory of the same name!");