proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;
--- a/src/Pure/Isar/toplevel.ML Mon Aug 07 23:43:19 2023 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Aug 08 12:35:14 2023 +0200
@@ -292,9 +292,9 @@
Runtime.controlled_execution (try generic_theory_of state)
(fn () =>
let
- val prev_thy = previous_theory_of state;
- val node_pr' = f (node_of state);
- in present_state true g node_pr' prev_thy end) ();
+ val node = node_of state;
+ val prev_thy = get_theory node;
+ in present_state true g (f node) prev_thy end) ();
fun apply_tr int trans state =
(case (trans, node_of state) of