TFL/rules.new.sml

--- 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;