TFL/post.sml
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