# HG changeset patch
# User wenzelm
# Date 911999045 -3600
# Node ID 0f7375e5e977cc427ff8520e356e75a91188672b
# Parent  6cf4e46ce95ae10978b2f9781ea664c716a4e6ab
replaced prs by writeln;

diff -r 6cf4e46ce95a -r 0f7375e5e977 TFL/post.sml
--- a/TFL/post.sml	Wed Nov 25 14:03:20 1998 +0100
+++ b/TFL/post.sml	Wed Nov 25 14:04:05 1998 +0100
@@ -138,16 +138,16 @@
   val gen_all = S.gen_all
 in
 fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
-  let val dummy = prs "Proving induction theorem..  "
+  let val dummy = writeln "Proving induction theorem..  "
       val ind = Prim.mk_induction theory f R full_pats_TCs
-      val dummy = prs "Proved induction theorem.\nPostprocessing..  "
+      val dummy = writeln "Proved induction theorem.\nPostprocessing..  "
       val {rules, induction, nested_tcs} = 
 	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => (writeln "Postprocessing done.";
             {induction=induction, rules=rules,tcs=[]})
-  | L  => let val dummy = prs "Simplifying nested TCs..  "
+  | L  => let val dummy = writeln "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
@@ -231,13 +231,13 @@
 local structure R = Rules
 in
 fun function theory eqs = 
- let val dummy = prs "Making definition..   "
+ let val dummy = writeln "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 dummy = prs "Definition made.\n"
-     val dummy = prs "Proving induction theorem..  "
+     val dummy = writeln "Definition made."
+     val dummy = writeln "Proving induction theorem..  "
      val induction = Prim.mk_induction theory f R full_pats_TCs
-     val dummy = prs "Induction theorem proved.\n"
+     val dummy = writeln "Induction theorem proved."
  in {theory = theory, 
      eq_ind = standard (induction RS (rules RS conjI))}
  end
diff -r 6cf4e46ce95a -r 0f7375e5e977 TFL/rules.new.sml
--- a/TFL/rules.new.sml	Wed Nov 25 14:03:20 1998 +0100
+++ b/TFL/rules.new.sml	Wed Nov 25 14:04:05 1998 +0100
@@ -514,17 +514,14 @@
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
 
-fun say s = if !tracing then prs s else ();
+fun say s = if !tracing then writeln s else ();
 
 fun print_thms s L = 
-   (say s; 
-    map (fn th => say (string_of_thm th ^"\n")) L;
-    say"\n");
+  say (cat_lines (s :: map string_of_thm L));
 
 fun print_cterms s L = 
-   (say s; 
-    map (fn th => say (string_of_cterm th ^"\n")) L;
-    say"\n");
+  say (cat_lines (s :: map string_of_cterm L));
+
 
 (*---------------------------------------------------------------------------
  * General abstraction handlers, should probably go in USyntax.
@@ -639,24 +636,24 @@
      val cut_lemma' = (cut_lemma RS mp) RS eq_reflection
      fun prover mss thm =
      let fun cong_prover mss thm =
-         let val dummy = say "cong_prover:\n"
+         let val dummy = say "cong_prover:"
              val cntxt = prems_of_mss mss
-             val dummy = print_thms "cntxt:\n" cntxt
-             val dummy = say "cong rule:\n"
-             val dummy = say (string_of_thm thm^"\n")
+             val dummy = print_thms "cntxt:" cntxt
+             val dummy = say "cong rule:"
+             val dummy = say (string_of_thm thm)
              val dummy = thm_ref := (thm :: !thm_ref)
              val dummy = mss_ref := (mss :: !mss_ref)
              (* Unquantified eliminate *)
              fun uq_eliminate (thm,imp,sign) = 
                  let val tych = cterm_of sign
-                     val dummy = print_cterms "To eliminate:\n" [tych imp]
+                     val dummy = print_cterms "To eliminate:" [tych imp]
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
                      val mss' = add_prems(mss, map ASSUME ants)
                      val lhs_eq_lhs1 = Thm.rewrite_cterm(false,true,false)mss' prover lhs
                        handle _ => reflexive lhs
-                     val dummy = print_thms "proven:\n" [lhs_eq_lhs1]
+                     val dummy = print_thms "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
                   in
@@ -724,9 +721,9 @@
          end handle _ => None
 
         fun restrict_prover mss thm =
-          let val dummy = say "restrict_prover:\n"
+          let val dummy = say "restrict_prover:"
               val cntxt = rev(prems_of_mss mss)
-              val dummy = print_thms "cntxt:\n" cntxt
+              val dummy = print_thms "cntxt:" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
               fun genl tm = let val vlist = gen_rems (op aconv)
@@ -748,12 +745,12 @@
               val antl = case rcontext of [] => [] 
                          | _   => [S.list_mk_conj(map cncl rcontext)]
               val TC = genl(S.list_mk_imp(antl, A))
-              val dummy = print_cterms "func:\n" [cterm_of sign func]
-              val dummy = print_cterms "TC:\n" 
+              val dummy = print_cterms "func:" [cterm_of sign func]
+              val dummy = print_cterms "TC:" 
 		              [cterm_of sign (HOLogic.mk_Trueprop TC)]
               val dummy = tc_list := (TC :: !tc_list)
               val nestedp = is_some (S.find_term is_func TC)
-              val dummy = if nestedp then say"nested\n" else say"not_nested\n"
+              val dummy = if nestedp then say "nested" else say "not_nested"
               val dummy = term_ref := ([func,TC]@(!term_ref))
               val th' = if nestedp then raise RULES_ERR{func = "solver", 
                                                       mesg = "nested function"}