1.1 --- a/src/HOL/Orderings.thy	Mon Mar 30 14:07:30 2009 -0700
     1.2 +++ b/src/HOL/Orderings.thy	Mon Mar 30 23:12:13 2009 +0200
     1.3 @@ -384,15 +384,11 @@
     1.4  
     1.5  (** Diagnostic command **)
     1.6  
     1.7 -val print = Toplevel.unknown_context o
     1.8 -  Toplevel.keep (Toplevel.node_case
     1.9 -    (Context.cases (print_structures o ProofContext.init) print_structures)
    1.10 -    (print_structures o Proof.context_of));
    1.11 -
    1.12  val _ =
    1.13    OuterSyntax.improper_command "print_orders"
    1.14      "print order structures available to transitivity reasoner" OuterKeyword.diag
    1.15 -    (Scan.succeed (Toplevel.no_timing o print));
    1.16 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.17 +        Toplevel.keep (print_structures o Toplevel.context_of)));
    1.18  
    1.19  
    1.20  (** Setup **)

     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 14:07:30 2009 -0700
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 23:12:13 2009 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      Pure/Isar/isar_cmd.ML
     2.5      Author:     Markus Wenzel, TU Muenchen
     2.6  
     2.7 -Derived Isar commands.
     2.8 +Miscellaneous Isar commands.
     2.9  *)
    2.10  
    2.11  signature ISAR_CMD =
    2.12 @@ -298,7 +298,7 @@
    2.13  
    2.14  (* current working directory *)
    2.15  
    2.16 -fun cd path = Toplevel.imperative (fn () => (File.cd path));
    2.17 +fun cd path = Toplevel.imperative (fn () => File.cd path);
    2.18  val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
    2.19  
    2.20  
    2.21 @@ -344,10 +344,9 @@
    2.22  
    2.23  val print_theorems_theory = Toplevel.keep (fn state =>
    2.24    Toplevel.theory_of state |>
    2.25 -  (case Toplevel.previous_node_of state of
    2.26 -    SOME prev_node =>
    2.27 -      ProofDisplay.print_theorems_diff (ProofContext.theory_of (Toplevel.context_node prev_node))
    2.28 -  | _ => ProofDisplay.print_theorems));
    2.29 +  (case Toplevel.previous_context_of state of
    2.30 +    SOME prev => ProofDisplay.print_theorems_diff (ProofContext.theory_of prev)
    2.31 +  | NONE => ProofDisplay.print_theorems));
    2.32  
    2.33  val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
    2.34  

     3.1 --- a/src/Pure/Isar/toplevel.ML	Mon Mar 30 14:07:30 2009 -0700
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 30 23:12:13 2009 +0200
     3.3 @@ -8,21 +8,14 @@
     3.4  sig
     3.5    exception UNDEF
     3.6    type generic_theory
     3.7 -  type node
     3.8 -  val theory_node: node -> generic_theory option
     3.9 -  val proof_node: node -> ProofNode.T option
    3.10 -  val cases_node: (generic_theory -> 'a) -> (Proof.state -> 'a) -> node -> 'a
    3.11 -  val context_node: node -> Proof.context
    3.12    type state
    3.13    val toplevel: state
    3.14    val is_toplevel: state -> bool
    3.15    val is_theory: state -> bool
    3.16    val is_proof: state -> bool
    3.17    val level: state -> int
    3.18 -  val previous_node_of: state -> node option
    3.19 -  val node_of: state -> node
    3.20 -  val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    3.21    val presentation_context_of: state -> Proof.context
    3.22 +  val previous_context_of: state -> Proof.context option
    3.23    val context_of: state -> Proof.context
    3.24    val generic_theory_of: state -> generic_theory
    3.25    val theory_of: state -> theory
    3.26 @@ -170,8 +163,6 @@
    3.27  
    3.28  (* current node *)
    3.29  
    3.30 -fun previous_node_of (State (_, prev)) = Option.map #1 prev;
    3.31 -
    3.32  fun node_of (State (NONE, _)) = raise UNDEF
    3.33    | node_of (State (SOME (node, _), _)) = node;
    3.34  
    3.35 @@ -186,6 +177,9 @@
    3.36    | SOME node => context_node node
    3.37    | NONE => raise UNDEF);
    3.38  
    3.39 +fun previous_context_of (State (_, NONE)) = NONE
    3.40 +  | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev);
    3.41 +
    3.42  val context_of = node_case Context.proof_of Proof.context_of;
    3.43  val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
    3.44  val theory_of = node_case Context.theory_of Proof.theory_of;