# HG changeset patch
# User wenzelm
# Date 1723314059 -7200
# Node ID 5b8fccf0a48ae20ddb1b202febacc65c6344cfad
# Parent  a6da4485a842a39d0e67f7e3d046f13cea97a399
tuned;

diff -r a6da4485a842 -r 5b8fccf0a48a src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Sat Aug 10 20:20:52 2024 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Sat Aug 10 20:20:59 2024 +0200
@@ -480,7 +480,7 @@
     val tenv = Envir.term_env env;
     val tyenv = Envir.type_env env;
   in
-    forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv)
+    Vartab.forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) tenv
   end;
 
 fun term_eq_wrt (env1, env2) (t1, t2) =