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