src/HOL/HOL.thy
changeset 82364 5af097d05e99
parent 82363 3a7fc54b50ca
child 82661 8a02dd7fcb5d
--- a/src/HOL/HOL.thy	Thu Mar 27 14:33:08 2025 +0100
+++ b/src/HOL/HOL.thy	Thu Mar 27 16:35:41 2025 +0100
@@ -38,7 +38,7 @@
 val _ =
   Try.tool_setup
    {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
-    body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE []}
+    body = fn auto => fst o Try0.generic_try0 (if auto then Try0.Auto_Try else Try0.Try) NONE Try0.empty_facts}
 \<close>
 
 ML \<open>Plugin_Name.declare_setup \<^binding>\<open>extraction\<close>\<close>