print_theorems: more robust difference, even after finished proof;

--- 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;