changeset 3978 | 7e1cfed19d94 |
parent 3927 | 27c63b757af5 |
child 4097 | ddd1c18121e0 |
--- 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