# HG changeset patch
# User haftmann
# Date 1177084706 -7200
# Node ID 6eafeffe801c6f3836e9c0a020e5d0aa67bbb27a
# Parent  e4a3f49eb924c008bbcbae741c75af667ac56dff
repaired value restriction problem

diff -r e4a3f49eb924 -r 6eafeffe801c src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 20 17:58:25 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Apr 20 17:58:26 2007 +0200
@@ -82,7 +82,9 @@
   val name = "HOL/function_def/data";
   type T = (term * fundef_context_data) NetRules.T
 
-  val empty = NetRules.init (op aconv o pairself fst) fst;
+  val empty = NetRules.init
+    (op aconv o pairself fst : (term * fundef_context_data) * (term * fundef_context_data) -> bool)
+    fst;
   val copy = I;
   val extend = I;
   fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)