# HG changeset patch
# User paulson
# Date 864205104 -7200
# Node ID c93f54759539a27109c1f7d8b4d8f21122fdcfbd
# Parent  b873969b05d3cb01322a784a19256032b9230dc7
Basis library input/output primitives; \!simpset instead of HOL_ss

diff -r b873969b05d3 -r c93f54759539 TFL/rules.new.sml
--- a/TFL/rules.new.sml	Wed May 21 10:57:38 1997 +0200
+++ b/TFL/rules.new.sml	Wed May 21 10:58:24 1997 +0200
@@ -401,7 +401,7 @@
 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;
 
@@ -531,7 +531,7 @@
 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;