# HG changeset patch
# User wenzelm
# Date 924614392 -7200
# Node ID 837e645e14bd2a9b975b8329aaa406920c0590c2
# Parent  23602e214ebfc6eb5b3f2c7dd1d36381f56b3e9e
temporarily reverted to 1.24;

diff -r 23602e214ebf -r 837e645e14bd TFL/post.sml
--- a/TFL/post.sml	Tue Apr 20 14:38:17 1999 +0200
+++ b/TFL/post.sml	Tue Apr 20 15:19:52 1999 +0200
@@ -9,8 +9,6 @@
 signature TFL = 
   sig
    structure Prim : TFL_sig
-   val quiet_mode : bool ref
-   val message : string -> unit
 
    val tgoalw : theory -> thm list -> thm list -> thm list
    val tgoal: theory -> thm list -> thm list
@@ -42,13 +40,6 @@
  structure Prim = Prim
  structure S = USyntax
 
-
-(* messages *)
-
-val quiet_mode = ref false;
-fun message s = if ! quiet_mode then () else writeln s;
-
-
 (*---------------------------------------------------------------------------
  * Extract termination goals so that they can be put it into a goalstack, or 
  * have a tactic directly applied to them.
@@ -95,10 +86,11 @@
 fun define_i thy fid R eqs = 
   let val dummy = Theory.requires thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
-  in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
+  in (Prim.wfrec_definition0 thy fid R functional, pats)
   end;
 
-(*lcp's version: takes strings; doesn't return "thm"*)
+(*lcp's version: takes strings; doesn't return "thm" 
+        (whose signature is a draft and therefore useless) *)
 fun define thy fid R eqs = 
   let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
   in  define_i thy fid (read thy R) (map (read thy) eqs)  end
@@ -146,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 = message "Proving induction theorem..  "
+  let val dummy = writeln "Proving induction theorem..  "
       val ind = Prim.mk_induction theory f R full_pats_TCs
-      val dummy = message "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 [] => (message "Postprocessing done.";
+  of [] => (writeln "Postprocessing done.";
             {induction=induction, rules=rules,tcs=[]})
-  | L  => let val dummy = message "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
@@ -165,7 +157,7 @@
               val rewr = full_simplify (ss addsimps (solved @ simplified'));
               val induction' = rewr induction
               and rules'     = rewr rules
-              val dummy = message "Postprocessing done."
+              val dummy = writeln "Postprocessing done."
           in
           {induction = induction',
                rules = rules',
@@ -240,13 +232,13 @@
 local structure R = Rules
 in
 fun function theory eqs = 
- let val dummy = message "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 = message "Definition made."
-     val dummy = message "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 = message "Induction theorem proved."
+     val dummy = writeln "Induction theorem proved."
  in {theory = theory, 
      eq_ind = standard (induction RS (rules RS conjI))}
  end