# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# 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