# HG changeset patch
# User wenzelm
# Date 1180802138 -7200
# Node ID 209e32e7c91e8b18bb0f5f5d621e68e8dd162c75
# Parent  b12f1c03cc9ace06c5c8ce9e5a2fdee93b69e3b9
made SML/NJ happy;

diff -r b12f1c03cc9a -r 209e32e7c91e src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Sat Jun 02 18:05:34 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat Jun 02 18:35:38 2007 +0200
@@ -276,7 +276,7 @@
 structure Preprocessor = GenericDataFun
 (
   type T = preproc
-  val empty = empty_preproc check_defs
+  val empty : T = empty_preproc check_defs
   val extend = I
   fun merge _ (a, _) = a
 );