# HG changeset patch
# User wenzelm
# Date 1026305288 -7200
# Node ID 1f5745b76fb80774df9106e056396300397b81f5
# Parent  f130bcf2962078bd9aa1c93a5cef4f18747fcb1f
NameSpace.accesses';

diff -r f130bcf29620 -r 1f5745b76fb8 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 10 14:47:48 2002 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Jul 10 14:48:08 2002 +0200
@@ -721,7 +721,7 @@
     (* prepare print translation functions *)
 
     val field_tr's =
-      print_translation (distinct (flat (map NameSpace.accesses (full_moreN :: names))));
+      print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
 
 
     (* prepare declarations *)