merged

--- a/src/HOL/Orderings.thy	Mon Mar 30 14:07:30 2009 -0700
+++ b/src/HOL/Orderings.thy	Mon Mar 30 23:12:13 2009 +0200
@@ -384,15 +384,11 @@
 
 (** Diagnostic command **)
 
-val print = Toplevel.unknown_context o
-  Toplevel.keep (Toplevel.node_case
-    (Context.cases (print_structures o ProofContext.init) print_structures)
-    (print_structures o Proof.context_of));
-
 val _ =
   OuterSyntax.improper_command "print_orders"
     "print order structures available to transitivity reasoner" OuterKeyword.diag
-    (Scan.succeed (Toplevel.no_timing o print));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+        Toplevel.keep (print_structures o Toplevel.context_of)));
 
 
 (** Setup **)

--- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 14:07:30 2009 -0700
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 30 23:12:13 2009 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Isar/isar_cmd.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Derived Isar commands.
+Miscellaneous Isar commands.
 *)
 
 signature ISAR_CMD =
@@ -298,7 +298,7 @@
 
 (* current working directory *)
 
-fun cd path = Toplevel.imperative (fn () => (File.cd path));
+fun cd path = Toplevel.imperative (fn () => File.cd path);
 val pwd = Toplevel.imperative (fn () => writeln (Path.implode (File.pwd ())));
 
 
@@ -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 14:07:30 2009 -0700
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 30 23:12:13 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;