# HG changeset patch
# User ballarin
# Date 1191234304 -7200
# Node ID 33b7fbc073613dbc8b3bd9d80b2bb5f4df89de4e
# Parent  f0dba1cda0b58457eef4ae1b600eb638b4bb433d
Simplified interface for printing of interpretations.

diff -r f0dba1cda0b5 -r 33b7fbc07361 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Mon Oct 01 12:24:45 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Oct 01 12:25:04 2007 +0200
@@ -457,9 +457,9 @@
 
 fun print_registrations show_wits name = Toplevel.unknown_context o
   Toplevel.keep (Toplevel.node_case
-      (Context.cases (Locale.print_global_registrations show_wits name)
-        (Locale.print_local_registrations show_wits name))
-    (Locale.print_local_registrations show_wits name o Proof.context_of));
+      (Context.cases (Locale.print_registrations show_wits name o ProofContext.init)
+        (Locale.print_registrations show_wits name))
+    (Locale.print_registrations show_wits name o Proof.context_of));
 
 val print_attributes = Toplevel.unknown_theory o
   Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of);