# HG changeset patch # User Fabian Huch # Date 1731086035 -3600 # Node ID 8abdd60acd60245cf57f00fb949977f13afd44f9 # Parent 895a4626fba3837c727bc600a8c63ddda0ba5b4d try0: avoid mapping background theory -- should be handled by Context_Position visibility; diff -r 895a4626fba3 -r 8abdd60acd60 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Oct 31 11:35:24 2024 +0100 +++ b/src/HOL/Tools/try0.ML Fri Nov 08 18:13:55 2024 +0100 @@ -142,11 +142,7 @@ |> Simplifier_Trace.disable |> Context_Position.set_visible false |> Config.put Unify.unify_trace false - |> Config.put Argo_Tactic.trace "none" - |> Proof_Context.background_theory (fn thy => - thy - |> Context_Position.set_visible_global false - |> Config.put_global Unify.unify_trace false)) + |> Config.put Argo_Tactic.trace "none") fun generic_try0 mode timeout_opt tagged st = let