NameSpace.accesses';
authorwenzelm
Wed Jul 10 14:48:08 2002 +0200 (2002-07-10 ago)
changeset 133331f5745b76fb8
parent 13332 f130bcf29620
child 13334 27149d72bdff
NameSpace.accesses';
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Wed Jul 10 14:47:48 2002 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Wed Jul 10 14:48:08 2002 +0200
     1.3 @@ -721,7 +721,7 @@
     1.4      (* prepare print translation functions *)
     1.5  
     1.6      val field_tr's =
     1.7 -      print_translation (distinct (flat (map NameSpace.accesses (full_moreN :: names))));
     1.8 +      print_translation (distinct (flat (map NameSpace.accesses' (full_moreN :: names))));
     1.9  
    1.10  
    1.11      (* prepare declarations *)