diff -r 1b052426a2b7 -r 72631efa3821 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Thu Sep 28 19:40:20 2023 +0200
+++ b/src/HOL/Metis.thy	Thu Sep 28 20:07:30 2023 +0200
@@ -10,7 +10,10 @@
 imports ATP
 begin
 
-ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+context notes [[ML_catch_all]]
+begin
+  ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+end
 
 
 subsection \<open>Literal selection and lambda-lifting helpers\<close>