changeset 3556 | 229a40c2b19e |
parent 3405 | 2cccd0e3e9ea |
child 3629 | 8e95bd329fff |
--- a/TFL/rules.new.sml Wed Jul 23 10:22:48 1997 +0200 +++ b/TFL/rules.new.sml Wed Jul 23 10:34:18 1997 +0200 @@ -393,7 +393,7 @@ local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None)) in fun simpl_conv ss thl ctm = - rew_conv (Thm.mss_of (#simps(rep_ss ss)@thl)) ctm + rew_conv (Thm.mss_of (#simps (Thm.dest_mss (#mss (rep_ss ss))) @ thl)) ctm RS meta_eq_to_obj_eq end;