# HG changeset patch
# User wenzelm
# Date 1294574160 -3600
# Node ID 820034384c18e0b4ae8ed810ff820953a60efe89
# Parent  9908cf4af3946b963e959cf5df4d640c6ea7e9e1
refined comment (again);

diff -r 9908cf4af394 -r 820034384c18 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sat Jan 08 11:29:25 2011 -0800
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Jan 09 12:56:00 2011 +0100
@@ -66,7 +66,7 @@
   type T = (int * run_action * done_action) list
   val empty = []
   val extend = I
-  fun merge data = Library.merge (K true) data  (* FIXME exponential blowup because of (K true) *)
+  fun merge data = Library.merge (K true) data  (* FIXME potential data loss because of (K true) *)
 )