diff -r fb49af893986 -r c32ebdcbe8ca src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Dec 02 11:08:36 2024 +0100 +++ b/src/Pure/Pure.thy Mon Dec 02 11:22:44 2024 +0100 @@ -1378,10 +1378,8 @@ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => - let - val thy = Toplevel.theory_of st; - val ctxt = Toplevel.context_of st; - in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); + let val ctxt = Toplevel.context_of st + in Pretty.writeln (Thm_Deps.pretty_thm_deps ctxt (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\