# HG changeset patch
# User wenzelm
# Date 968259697 -7200
# Node ID a1fcaf2d080d4d06851cfa0956fa0487320ccaa3
# Parent  b145613939c1e0605189eadf9a0a05dc6c02d0a6
make SML/NJ happy;

diff -r b145613939c1 -r a1fcaf2d080d src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Sep 06 17:58:37 2000 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Wed Sep 06 19:01:37 2000 +0200
@@ -105,7 +105,7 @@
   val name = "HOL/recdef";
   type T = recdef_info Symtab.table * hints;
 
-  val empty = (Symtab.empty, mk_hints ([], [], []));
+  val empty = (Symtab.empty, mk_hints ([], [], [])): T;
   val copy = I;
   val prep_ext = I;
   fun merge