# HG changeset patch
# User wenzelm
# Date 1165353288 -3600
# Node ID 734a9c3f562d7945421d62ecb466b80b8e04106d
# Parent  ab802d4eaaf46f05785c27ee63158008696b3079
print_syntax etc.: plain Toplevel.context_of;

diff -r ab802d4eaaf4 -r 734a9c3f562d src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Dec 05 22:14:47 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Dec 05 22:14:48 2006 +0100
@@ -334,9 +334,8 @@
 fun print_theory verbose = Toplevel.unknown_theory o
   Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
 
-val print_syntax = Toplevel.unknown_theory o
-  Toplevel.keep (Display.print_syntax o Toplevel.theory_of) o
-  Toplevel.keep (ProofContext.print_syntax o Proof.context_of o Toplevel.proof_of);
+val print_syntax = Toplevel.unknown_context o
+  Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);
 
 val print_facts = Toplevel.unknown_context o Toplevel.keep (fn state =>
   ProofContext.setmp_verbose
@@ -352,7 +351,7 @@
     SOME (SOME prev_thy) => ProofDisplay.print_theorems_diff (Context.theory_of prev_thy)
   | _ => ProofDisplay.print_theorems));
 
-val print_theorems = Toplevel.unknown_theory o print_theorems_theory o print_theorems_proof;
+val print_theorems = Toplevel.unknown_context o print_theorems_theory o print_theorems_proof;
 
 val print_locales = Toplevel.unknown_theory o
   Toplevel.keep (Locale.print_locales o Toplevel.theory_of);
@@ -418,13 +417,11 @@
 
 (* print proof context contents *)
 
-val print_binds = Toplevel.unknown_proof o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
-    ProofContext.print_binds (Proof.context_of (Toplevel.proof_of state)));
+val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
+  ProofContext.setmp_verbose ProofContext.print_binds (Toplevel.context_of state));
 
-val print_cases = Toplevel.unknown_proof o Toplevel.keep (fn state =>
-  ProofContext.setmp_verbose
-    ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
+val print_cases = Toplevel.unknown_context o Toplevel.keep (fn state =>
+  ProofContext.setmp_verbose ProofContext.print_cases (Toplevel.context_of state));
 
 
 (* print theorems, terms, types etc. *)