--- a/src/Pure/Isar/isar_cmd.ML Fri Dec 12 20:03:30 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Fri Dec 12 20:10:22 2008 +0100
@@ -346,8 +346,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;