# HG changeset patch
# User wenzelm
# Date 883317910 -3600
# Node ID 34a53d0c8e8dbe08c64f541de614b2f110b5d297
# Parent  14cd07c16e029d35c0bb3cc73fcf07cc680deb4c
Symtab.empty;

diff -r 14cd07c16e02 -r 34a53d0c8e8d src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Sun Dec 28 15:00:20 1997 +0100
+++ b/src/HOL/thy_data.ML	Sun Dec 28 15:05:10 1997 +0100
@@ -46,7 +46,7 @@
 exception DatatypeInfo of datatype_info Symtab.table;
 
 local
-  val empty = DatatypeInfo Symtab.null;
+  val empty = DatatypeInfo Symtab.empty;
 
   fun prep_ext (x as DatatypeInfo _) = x;
 
@@ -86,7 +86,7 @@
 (* methods *)
 
 local
-  val empty = Records Symtab.null;
+  val empty = Records Symtab.empty;
 
   fun prep_ext (x as Records _) = x;