--- 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