# HG changeset patch
# User wenzelm
# Date 1691490914 -7200
# Node ID 44ffc06187e0ef92baf2c18221ce4c018e6f3be0
# Parent  e72f8009a4f0b719d3c1a4cf62eb2ef60e5bfca3
proper prev_thy (amending 92a547feec88), notably for the sake of 'print_theorems', which is the only use of Toplevel.previous_theory_of;

diff -r e72f8009a4f0 -r 44ffc06187e0 src/Pure/Isar/toplevel.ML
--- 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