# HG changeset patch
# User wenzelm
# Date 1118311402 -7200
# Node ID 37aabcf75ee1662ffb6cabc386fb88fe38c6c98b
# Parent  b773132e3715c24f4d30dbc5f3ffd8596013e0ba
NameSpace.extern_table;

diff -r b773132e3715 -r 37aabcf75ee1 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Thu Jun 09 12:03:21 2005 +0200
+++ b/src/Pure/goals.ML	Thu Jun 09 12:03:22 2005 +0200
@@ -198,7 +198,7 @@
 
   fun print sg {space, locales, scope} =
     let
-      val locs = NameSpace.extern_table space locales;
+      val locs = NameSpace.extern_table (space, locales);
       val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
     in
       [Display.pretty_name_space ("locale name space", space),