# HG changeset patch
# User wenzelm
# Date 1229013157 -3600
# Node ID 9c98e197a1430534fffcaf9bd0e13b5954abf49e
# Parent  f50c24e5b9fefd513c459f79d16f0f33aeee5cb2
print_theorems: more robust difference, even after finished proof;

diff -r f50c24e5b9fe -r 9c98e197a143 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 17:31:23 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Dec 11 17:32:37 2008 +0100
@@ -347,8 +347,9 @@
 
 val print_theorems_theory = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
-  (case Option.map Toplevel.theory_node (Toplevel.previous_node_of state) of
-    SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy)
+  (case Toplevel.previous_node_of state of
+    SOME prev_node =>
+      ProofDisplay.print_theorems_diff (ProofContext.theory_of (Toplevel.context_node prev_node))
   | _ => ProofDisplay.print_theorems));
 
 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;