# HG changeset patch
# User wenzelm
# Date 877603679 -7200
# Node ID 7e1cfed19d946a79b0b352c78ec68843212c2428
# Parent  9b3cbfd6a93637b13fe4d14621150280e74e9c92
Sign.stamp_names_of;

diff -r 9b3cbfd6a936 -r 7e1cfed19d94 TFL/post.sml
--- a/TFL/post.sml	Thu Oct 23 12:44:46 1997 +0200
+++ b/TFL/post.sml	Thu Oct 23 12:47:59 1997 +0200
@@ -193,7 +193,7 @@
 val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
 
 fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
-   let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
+   let val dummy = deny (id mem (Sign.stamp_names_of (sign_of thy)))
                         ("Recursive definition " ^ id ^ 
                          " would clash with the theory of the same name!")
        val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
diff -r 9b3cbfd6a936 -r 7e1cfed19d94 src/HOL/intr_elim.ML
--- a/src/HOL/intr_elim.ML	Thu Oct 23 12:44:46 1997 +0200
+++ b/src/HOL/intr_elim.ML	Thu Oct 23 12:47:59 1997 +0200
@@ -45,7 +45,7 @@
 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
 val big_rec_name = space_implode "_" rec_names;
 
-val _ = deny (big_rec_name  mem  map ! (stamps_of_thy Inductive.thy))
+val _ = deny (big_rec_name mem (Sign.stamp_names_of (sign_of Inductive.thy)))
              ("Definition " ^ big_rec_name ^ 
               " would clash with the theory of the same name!");
 
diff -r 9b3cbfd6a936 -r 7e1cfed19d94 src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Thu Oct 23 12:44:46 1997 +0200
+++ b/src/ZF/intr_elim.ML	Thu Oct 23 12:47:59 1997 +0200
@@ -50,7 +50,7 @@
 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms;
 val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names);
 
-val _ = deny (big_rec_base_name  mem  map ! (stamps_of_thy Inductive.thy))
+val _ = deny (big_rec_base_name mem (Sign.stamp_names_of (sign_of Inductive.thy)))
              ("Definition " ^ big_rec_base_name ^ 
               " would clash with the theory of the same name!");