Simplified interface for printing of interpretations.
authorballarin
Mon, 01 Oct 2007 12:25:04 +0200
changeset 24789 33b7fbc07361
parent 24788 f0dba1cda0b5
child 24790 3be1580de4cc
Simplified interface for printing of interpretations.
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);