diff -r 71c45d60a90a -r a63d76ba0a03 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Wed May 12 06:35:16 2021 +0200
+++ b/src/HOL/Sledgehammer.thy	Wed May 12 12:22:44 2021 +0200
@@ -33,5 +33,6 @@
 ML_file \<open>Tools/Sledgehammer/sledgehammer_mash.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer.ML\<close>
 ML_file \<open>Tools/Sledgehammer/sledgehammer_commands.ML\<close>
+ML_file \<open>Tools/Sledgehammer/sledgehammer_tactics.ML\<close>
 
 end