# HG changeset patch
# User wenzelm
# Date 1583766773 -3600
# Node ID 82fbfccca7dd0d63836b1608d8974285c26012dd
# Parent  50ac132a49bbbc8b3f15f3b00869a66fc90522b0
tuned;

diff -r 50ac132a49bb -r 82fbfccca7dd src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Mon Mar 09 15:50:24 2020 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 09 16:12:53 2020 +0100
@@ -1877,7 +1877,7 @@
     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 env' = solve thy cs' env
+    val env' = solve thy cs' env;
   in thawf (norm_proof env' prf) end handle MIN_PROOF () => MinProof;
 
 fun prop_of_atom prop Ts =
@@ -2055,10 +2055,10 @@
 
 fun standard_hidden_terms term proof =
   let
-    fun add_not excl x =
-      ((is_Free x orelse is_Var x) andalso not (member (op =) excl x)) ? insert (op =) x;
-    val visible = fold_aterms (add_not []) term [];
-    val hidden = fold_proof_terms (fold_aterms (add_not visible)) proof [];
+    fun add_unless excluded x =
+      ((is_Free x orelse is_Var x) andalso not (member (op =) excluded x)) ? insert (op =) x;
+    val visible = fold_aterms (add_unless []) term [];
+    val hidden = fold_proof_terms (fold_aterms (add_unless visible)) proof [];
     val dummy_term = Term.map_aterms (fn x =>
       if member (op =) hidden x then Term.dummy_pattern (Term.fastype_of x) else x);
   in proof |> not (null hidden) ? map_proof_terms dummy_term I end;