NameSpace.extern_table;
authorwenzelm
Thu, 09 Jun 2005 12:03:22 +0200
changeset 16335 37aabcf75ee1
parent 16334 b773132e3715
child 16336 e3892698c57d
NameSpace.extern_table;
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),