| changeset 33095 | bbd52d2f8696 |
| parent 33063 | 4d462963a7db |
| child 33368 | b1cf34f1855c |
--- a/src/HOL/Tools/record.ML Sat Oct 24 19:24:50 2009 +0200 +++ b/src/HOL/Tools/record.ML Sat Oct 24 19:47:37 2009 +0200 @@ -1810,7 +1810,7 @@ fun record_definition (args, bname) parent (parents: parent_info list) raw_fields thy = let - val external_names = NameSpace.external_names (Sign.naming_of thy); + val external_names = Name_Space.external_names (Sign.naming_of thy); val alphas = map fst args; val name = Sign.full_bname thy bname;