# HG changeset patch # User wenzelm # Date 870869705 -7200 # Node ID 8e95bd329fffbf79d9b7dacb7249edc8745ce86a # Parent 41a49c67190186386a781d976a1fdbe71aa1c57b prs instead of TextIO.output; diff -r 41a49c671901 -r 8e95bd329fff TFL/rules.new.sml --- a/TFL/rules.new.sml Wed Aug 06 14:12:29 1997 +0200 +++ b/TFL/rules.new.sml Wed Aug 06 14:15:05 1997 +0200 @@ -514,7 +514,7 @@ val thm_ref = ref [] : thm list ref; val tracing = ref false; -fun say s = if !tracing then TextIO.output (TextIO.stdOut, s) else (); +fun say s = if !tracing then prs s else (); fun print_thms s L = (say s;