TFL/rules.new.sml

    rewrite_rule (map (fn th => (th RS eq_reflection) handle _ => th) thl);
 
 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;
 
 local fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1])
 in