1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 21:54:15 2009 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 22:38:50 2009 +0200
     1.3 @@ -344,10 +344,9 @@
     1.4  
     1.5  val print_theorems_theory = Toplevel.keep (fn state =>
     1.6    Toplevel.theory_of state |>
     1.7 -  (case Toplevel.previous_node_of state of
     1.8 -    SOME prev_node =>
     1.9 -      ProofDisplay.print_theorems_diff (ProofContext.theory_of (Toplevel.context_node prev_node))
    1.10 -  | _ => ProofDisplay.print_theorems));
    1.11 +  (case Toplevel.previous_context_of state of
    1.12 +    SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
    1.13 +  | NONE => ProofDisplay.print_theorems));
    1.14  
    1.15  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
    1.16  

     2.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 30 21:54:15 2009 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 30 22:38:50 2009 +0200
     2.3 @@ -8,21 +8,14 @@
     2.4  sig
     2.5    exception UNDEF
     2.6    type generic_theory
     2.7 -  type node
     2.8 -  val theory_node: node -> generic_theory option
     2.9 -  val proof_node: node -> ProofNode.T option
    2.10 -  val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
    2.11 -  val context_node: node -> Proof.context
    2.12    type state
    2.13    val toplevel: state
    2.14    val is_toplevel: state -> bool
    2.15    val is_theory: state -> bool
    2.16    val is_proof: state -> bool
    2.17    val level: state -> int
    2.18 -  val previous_node_of: state -> node option
    2.19 -  val node_of: state -> node
    2.20 -  val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    2.21    val presentation_context_of: state -> Proof.context
    2.22 +  val previous_context_of: state -> Proof.context option
    2.23    val context_of: state -> Proof.context
    2.24    val generic_theory_of: state -> generic_theory
    2.25    val theory_of: state -> theory
    2.26 @@ -170,8 +163,6 @@
    2.27  
    2.28  (* current node *)
    2.29  
    2.30 -fun previous_node_of (State (_, prev)) = Option.map #1 prev;
    2.31 -
    2.32  fun node_of (State (NONE, _)) = raise UNDEF
    2.33    | node_of (State (SOME (node, _), _)) = node;
    2.34  
    2.35 @@ -186,6 +177,9 @@
    2.36    | SOME node => context_node node
    2.37    | NONE => raise UNDEF);
    2.38  
    2.39 +fun previous_context_of (State (_, NONE)) = NONE
    2.40 +  | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
    2.41 +
    2.42  val context_of = node_case Context.proof_of Proof.context_of;
    2.43  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
    2.44  val theory_of = node_case Context.theory_of Proof.theory_of;