# HG changeset patch
# User wenzelm
# Date 1662377529 -7200
# Node ID 98610c8e9caaf44de0a37882d1b941ceb896b425
# Parent  7cf72240cdd476c98c96dead4725a2c703a9dccf
tuned;

diff -r 7cf72240cdd4 -r 98610c8e9caa src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 05 11:36:41 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 05 13:32:09 2022 +0200
@@ -992,8 +992,10 @@
   let
     val var_props = take_prefix is_var props;
     val explicit_vars = fold Term.add_vars var_props [];
-    val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
-  in map (Logic.mk_term o Var) vars end;
+  in
+    fold Term.add_vars props [] |> map_filter (fn v =>
+      if member (op =) explicit_vars v then NONE else SOME (Logic.mk_term (Var v)))
+  end;
 
 fun refine_terms n =
   refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o