# HG changeset patch
# User wenzelm
# Date 1160177462 -7200
# Node ID 1316db4819440f78de5c3466b4ebe202f5c422b1
# Parent  4066ee15b278ef106cf425c55db41226c5e262e8
tuned comments;

diff -r 4066ee15b278 -r 1316db481944 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Sat Oct 07 01:31:01 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat Oct 07 01:31:02 2006 +0200
@@ -200,6 +200,7 @@
     val empty = []
     val extend = I
     fun merge _ (l1, l2) = l1 @ l2
+      (* FIXME exponential blowup! cf. Library.merge, Drule.merge_rules *)
     fun print  _ _ = ()
 end);