author | wenzelm |
Thu, 09 Jun 2005 12:03:22 +0200 | |
changeset 16335 | 37aabcf75ee1 |
parent 16334 | b773132e3715 |
child 16336 | e3892698c57d |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- 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),