# HG changeset patch
# User wenzelm
# Date 1346332941 -7200
# Node ID a3cdb49c22ccf8c223f8824acb4e54ee73b6e6da
# Parent  f781bbe0d91b76daf283b41c2c0756c0d069e04f
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

diff -r f781bbe0d91b -r a3cdb49c22cc src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Aug 29 22:18:33 2012 +0200
+++ b/src/Pure/thm.ML	Thu Aug 30 15:22:21 2012 +0200
@@ -514,7 +514,7 @@
 
 fun join_promises [] = ()
   | join_promises promises = join_promises_of (Future.joins (map snd promises))
-and join_promises_of thms = join_promises (maps raw_promises_of thms);
+and join_promises_of thms = join_promises (Ord_List.make promise_ord (maps raw_promises_of thms));
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body