TFL/rules.new.sml

 val simplify = rewrite_rule;
 
 local fun rew_conv mss = rewrite_cterm (true,false) mss (K(K None))
 in
 fun simpl_conv thl ctm = 
- rew_conv (Thm.mss_of (#simps(rep_ss HOL_ss)@thl)) ctm
+ rew_conv (Thm.mss_of (#simps(rep_ss (!simpset))@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

 val term_ref = ref[] : term list ref
 val mss_ref = ref [] : meta_simpset list ref;
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
 
-fun say s = if !tracing then (output(std_out,s); flush_out std_out) else ();
+fun say s = if !tracing then TextIO.output (TextIO.stdOut, s) else ();
 
 fun print_thms s L = 
    (say s; 
     map (fn th => say (string_of_thm th ^"\n")) L;
     say"\n");