--- 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
--- 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!");
--- 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!");