src/ZF/Tools/inductive_package.ML
changeset 16457 e0f22edf38a5
parent 15705 b5edb9dcec9a
child 16855 7563d0eb3414
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Jun 17 18:33:41 2005 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Jun 17 18:33:42 2005 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5    (*Forbid the inductive definition structure from clashing with a theory
     1.6      name.  This restriction may become obsolete as ML is de-emphasized.*)
     1.7 -  val dummy = deny (big_rec_base_name mem (Sign.stamp_names_of sign))
     1.8 +  val dummy = deny (big_rec_base_name mem (Context.names_of sign))
     1.9                 ("Definition " ^ big_rec_base_name ^
    1.10                  " would clash with the theory of the same name!");
    1.11