1.1 --- a/src/HOL/thy_syntax.ML	Wed Apr 29 11:43:53 1998 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Apr 29 11:44:30 1998 +0200
     1.3 @@ -292,8 +292,8 @@
     1.4  
     1.5  val _ = ThySyn.add_syntax
     1.6   ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
     1.7 - [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
     1.8 -  (section "record" "|> Record.add_record" record_decl),
     1.9 + [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
    1.10 +  (section "record" "|> RecordPackage.add_record" record_decl),
    1.11    ("inductive", inductive_decl ""),
    1.12    ("coinductive", inductive_decl "Co"),
    1.13    (section "datatype" "" datatype_decl),