merged

--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 21:54:15 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 22:38:50 2009 +0200
@@ -344,10 +344,9 @@
 
 val print_theorems_theory = Toplevel.keep (fn state =>
   Toplevel.theory_of state |>
-  (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));
+  (case Toplevel.previous_context_of state of
+    SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
+  | NONE => ProofDisplay.print_theorems));
 
 val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
 

--- a/src/Pure/Isar/toplevel.ML	Mon Mar 30 21:54:15 2009 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 30 22:38:50 2009 +0200
@@ -8,21 +8,14 @@
 sig
   exception UNDEF
   type generic_theory
-  type node
-  val theory_node: node -> generic_theory option
-  val proof_node: node -> ProofNode.T option
-  val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
-  val context_node: node -> Proof.context
   type state
   val toplevel: state
   val is_toplevel: state -> bool
   val is_theory: state -> bool
   val is_proof: state -> bool
   val level: state -> int
-  val previous_node_of: state -> node option
-  val node_of: state -> node
-  val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   val presentation_context_of: state -> Proof.context
+  val previous_context_of: state -> Proof.context option
   val context_of: state -> Proof.context
   val generic_theory_of: state -> generic_theory
   val theory_of: state -> theory
@@ -170,8 +163,6 @@
 
 (* current node *)
 
-fun previous_node_of (State (_, prev)) = Option.map #1 prev;
-
 fun node_of (State (NONE, _)) = raise UNDEF
   | node_of (State (SOME (node, _), _)) = node;
 
@@ -186,6 +177,9 @@
   | SOME node => context_node node
   | NONE => raise UNDEF);
 
+fun previous_context_of (State (_, NONE)) = NONE
+  | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
+
 val context_of = node_case Context.proof_of Proof.context_of;
 val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
 val theory_of = node_case Context.theory_of Proof.theory_of;