# HG changeset patch
# User wenzelm
# Date 893843070 -7200
# Node ID b5999638979e1dc2549bc30a14df1f61659a4297
# Parent  33e7cdc20681ef5418501e5079a40422700d284d
TypedefPackage.add_typedef;
RecordPackage.add_record;

diff -r 33e7cdc20681 -r b5999638979e src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Wed Apr 29 11:43:53 1998 +0200
+++ b/src/HOL/thy_syntax.ML	Wed Apr 29 11:44:30 1998 +0200
@@ -292,8 +292,8 @@
 
 val _ = ThySyn.add_syntax
  ["intrs", "monos", "con_defs", "congs", "simpset", "|"]
- [axm_section "typedef" "|> Typedef.add_typedef" typedef_decl,
-  (section "record" "|> Record.add_record" record_decl),
+ [axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl,
+  (section "record" "|> RecordPackage.add_record" record_decl),
   ("inductive", inductive_decl ""),
   ("coinductive", inductive_decl "Co"),
   (section "datatype" "" datatype_decl),