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