--- a/src/Pure/Proof/reconstruct.ML Tue Jul 30 11:51:55 2019 +0200
+++ b/src/Pure/Proof/reconstruct.ML Tue Jul 30 13:19:14 2019 +0200
@@ -6,7 +6,6 @@
signature RECONSTRUCT =
sig
- val quiet_mode: bool Config.T
val reconstruct_proof: Proof.context -> term -> Proofterm.proof -> Proofterm.proof
val prop_of': term list -> Proofterm.proof -> term
val prop_of: Proofterm.proof -> term
@@ -17,12 +16,6 @@
structure Reconstruct : RECONSTRUCT =
struct
-val quiet_mode = Config.declare_bool ("Reconstruct.quiet_mode", \<^here>) (K true);
-
-fun message ctxt msg =
- if Config.get ctxt quiet_mode then () else writeln (msg ());
-
-
(* generate constraints for proof term *)
fun mk_var env Ts T =
@@ -278,15 +271,11 @@
fun reconstruct_proof ctxt prop cprf =
let
val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop);
- val _ = message ctxt (fn _ => "Collecting constraints ...");
val (t, prf, cs, env, _) = make_constraints_cprf ctxt
(Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
val cs' =
map (apply2 (Envir.norm_term env)) ((t, prop') :: cs)
|> map (fn p => (true, p, Term.add_var_names (#1 p) (Term.add_var_names (#2 p) [])));
- val _ =
- message ctxt
- (fn () => "Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
val env' = solve ctxt cs' env
in
thawf (Proofterm.norm_proof env' prf)
@@ -348,9 +337,6 @@
(case AList.lookup (op =) prfs (a, prop) of
NONE =>
let
- val _ =
- message ctxt (fn () =>
- "Reconstructing proof of " ^ a ^ "\n" ^ Syntax.string_of_term ctxt prop);
val prf' =
Proofterm.join_proof body
|> open_proof