proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

--- 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