TFL/post.sml
changeset 3978 7e1cfed19d94
parent 3927 27c63b757af5
child 4097 ddd1c18121e0
equal deleted inserted replaced
3977:9b3cbfd6a936 3978:7e1cfed19d94
   191  * have already been added in thry.sml
   191  * have already been added in thry.sml
   192  *---------------------------------------------------------------------------*)
   192  *---------------------------------------------------------------------------*)
   193 val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
   193 val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
   194 
   194 
   195 fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
   195 fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
   196    let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
   196    let val dummy = deny (id mem (Sign.stamp_names_of (sign_of thy)))
   197                         ("Recursive definition " ^ id ^ 
   197                         ("Recursive definition " ^ id ^ 
   198                          " would clash with the theory of the same name!")
   198                          " would clash with the theory of the same name!")
   199        val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
   199        val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
   200        val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
   200        val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
   201        val {theory,rules,TCs,full_pats_TCs,patterns} = 
   201        val {theory,rules,TCs,full_pats_TCs,patterns} =