# HG changeset patch
# User wenzelm
# Date 957558880 -7200
# Node ID 1c48b3732399a1b2001bbf032089bc71cf1a6f2e
# Parent  31b4fb3d8d6078c1bd2d8e328758c06a274fdcb0
tuned messages;
use Sign.simple_read_term;

diff -r 31b4fb3d8d60 -r 1c48b3732399 TFL/post.sml
--- a/TFL/post.sml	Fri May 05 22:32:49 2000 +0200
+++ b/TFL/post.sml	Fri May 05 22:34:40 2000 +0200
@@ -48,6 +48,9 @@
  structure Prim = Prim
  structure S = USyntax
 
+ fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT;
+
+
  (* messages *)
 
  val quiet_mode = ref false;
@@ -55,6 +58,7 @@
 
  val trace = Prim.trace
 
+
  (*---------------------------------------------------------------------------
   * Extract termination goals so that they can be put it into a goalstack, or 
   * have a tactic directly applied to them.
@@ -141,14 +145,12 @@
    let val dummy = message "Proving induction theorem ..."
        val ind = Prim.mk_induction theory 
                     {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
-       val dummy = (message "Proved induction theorem."; 
-		    message "Postprocessing ...");
+       val dummy = message "Postprocessing ...";
        val {rules, induction, nested_tcs} = 
 	   std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
    in
    case nested_tcs
-   of [] => (message "Postprocessing done.";
-	     {induction=induction, rules=rules,tcs=[]})
+   of [] => {induction=induction, rules=rules,tcs=[]}
    | L  => let val dummy = message "Simplifying nested TCs ..."
 	       val (solved,simplified,stubborn) =
 		U.itlist (fn th => fn (So,Si,St) =>
@@ -159,7 +161,6 @@
 	       val rewr = full_simplify (ss addsimps (solved @ simplified'));
 	       val induction' = rewr induction
 	       and rules'     = rewr rules
-	       val dummy = message "Postprocessing done."
 	   in
 	   {induction = induction',
 		rules = rules',
@@ -187,7 +188,7 @@
  fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
     let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
 			 ("Recursive definition " ^ id ^ 
-			  " would clash with the theory of the same name!")
+			  " would clash with the theory of the same name!")	(* FIXME !? *)
 	val def = freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
 	val {theory,rules,rows,TCs,full_pats_TCs} = 
 		 Prim.post_definition (Prim.congs tflCongs)
@@ -220,10 +221,8 @@
    end;
 
  fun define thy fid R ss_congs seqs = 
-   let val _ =  writeln ("Recursive function " ^ fid)
-       val read = readtm (Theory.sign_of thy) HOLogic.termT;
-   in  define_i thy fid (read R) ss_congs (map read seqs)  end
-   handle Utils.ERR {mesg,...} => error mesg;
+   define_i thy fid (read_term thy R) ss_congs (map (read_term thy) seqs)
+     handle Utils.ERR {mesg,...} => error mesg;
 
 
 (*---------------------------------------------------------------------------
@@ -242,11 +241,9 @@
   let val {rules,R,theory,full_pats_TCs,SV,...} = 
 	      Prim.lazyR_def thy (Sign.base_name fid) congs eqs
       val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
-      val dummy = (message "Definition made."; 
-		   message "Proving induction theorem ...");
+      val dummy = message "Proving induction theorem ...";
       val induction = Prim.mk_induction theory 
                          {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
-      val dummy = message "Induction theorem proved."
   in (theory, 
       (*return the conjoined induction rule and recursion equations, 
 	with assumptions remaining to discharge*)
@@ -254,9 +251,8 @@
   end
 
  fun defer thy fid congs seqs = 
-   let val read = readtm (Theory.sign_of thy) HOLogic.termT;
-   in  defer_i thy fid congs (map read seqs)  end
-   handle Utils.ERR {mesg,...} => error mesg;
+   defer_i thy fid congs (map (read_term thy) seqs)
+     handle Utils.ERR {mesg,...} => error mesg;
  end;
 
 end;