# HG changeset patch
# User paulson
# Date 852284731 -3600
# Node ID 357adb429fda3166565f8daefc0f4f151c6f3271
# Parent  5220fb014f8a54e88d8babd85234a32ed6e0ea8e
Conversion to Basis Library (using prs instead of output)

diff -r 5220fb014f8a -r 357adb429fda TFL/ROOT.ML
--- a/TFL/ROOT.ML	Fri Dec 20 16:10:30 1996 +0100
+++ b/TFL/ROOT.ML	Fri Jan 03 10:45:31 1997 +0100
@@ -8,4 +8,5 @@
 *)
 
 use"sys.sml";
-use_dir"examples/Subst";
+cd"examples/Subst";
+use"ROOT.ML";
diff -r 5220fb014f8a -r 357adb429fda TFL/post.sml
--- a/TFL/post.sml	Fri Dec 20 16:10:30 1996 +0100
+++ b/TFL/post.sml	Fri Jan 03 10:45:31 1997 +0100
@@ -112,26 +112,23 @@
   val gen_all = S.gen_all
 in
 fun rfunction theory reducer R eqs = 
- let val _ = output(std_out, "Making definition..  ")
-     val _ = flush_out std_out
+ let val _ = prs "Making definition..  "
      val {rules,theory, full_pats_TCs,
           TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} 
      val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules))
-     val _ = output(std_out, "Definition made.\n")
-     val _ = output(std_out, "Proving induction theorem..  ")
-     val _ = flush_out std_out
+     val _ = prs "Definition made.\n"
+     val _ = prs "Proving induction theorem..  "
      val ind = Prim.mk_induction theory f R full_pats_TCs
-     val _ = output(std_out, "Proved induction theorem.\n")
+     val _ = prs "Proved induction theorem.\n"
      val pp = std_postprocessor theory
-     val _ = output(std_out, "Postprocessing..  ")
-     val _ = flush_out std_out
+     val _ = prs "Postprocessing..  "
      val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
      val normal_tcs = Prim.termination_goals rules
  in
  case nested_tcs
- of [] => (output(std_out, "Postprocessing done.\n");
+ of [] => (prs "Postprocessing done.\n";
            {theory=theory, induction=induction, rules=rules,tcs=normal_tcs})
-  | L  => let val _ = output(std_out, "Simplifying nested TCs..  ")
+  | L  => let val _ = prs "Simplifying nested TCs..  "
               val (solved,simplified,stubborn) =
                U.itlist (fn th => fn (So,Si,St) =>
                      if (id_thm th) then (So, Si, th::St) else
@@ -140,7 +137,7 @@
               val simplified' = map join_assums simplified
               val induction' = reducer (solved@simplified') induction
               val rules' = reducer (solved@simplified') rules
-              val _ = output(std_out, "Postprocessing done.\n")
+              val _ = prs "Postprocessing done.\n"
           in
           {induction = induction',
                rules = rules',
@@ -165,13 +162,13 @@
 local structure R = Prim.Rules
 in
 fun function theory eqs = 
- let val _ = output(std_out, "Making definition..  ")
+ let val _ = prs "Making definition..  "
      val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
      val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
-     val _ = output(std_out, "Definition made.\n")
-     val _ = output(std_out, "Proving induction theorem..  ")
+     val _ = prs "Definition made.\n"
+     val _ = prs "Proving induction theorem..  "
      val induction = Prim.mk_induction theory f R full_pats_TCs
-      val _ = output(std_out, "Induction theorem proved.\n")
+     val _ = prs "Induction theorem proved.\n"
  in {theory = theory, 
      eq_ind = standard (induction RS (rules RS conjI))}
  end
diff -r 5220fb014f8a -r 357adb429fda TFL/rules.new.sml
--- a/TFL/rules.new.sml	Fri Dec 20 16:10:30 1996 +0100
+++ b/TFL/rules.new.sml	Fri Jan 03 10:45:31 1997 +0100
@@ -542,7 +542,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 prs s else ();
 
 fun print_thms s L = 
    (say s; 
diff -r 5220fb014f8a -r 357adb429fda TFL/utils.sml
--- a/TFL/utils.sml	Fri Dec 20 16:10:30 1996 +0100
+++ b/TFL/utils.sml	Fri Jan 03 10:45:31 1997 +0100
@@ -19,7 +19,7 @@
 val MESG_string = info_string "Message"
 end;
 
-fun Raise (e as ERR sss) = (output(std_out, ERR_string sss);  raise e)
+fun Raise (e as ERR sss) = (prs (ERR_string sss); raise e)
   | Raise e = raise e;