| changeset 49010 | 72808e956879 |
| parent 48992 | 0518bf89c777 |
| child 49011 | 9c68e43502ce |
--- a/src/Pure/Thy/thy_info.ML Thu Aug 30 15:26:37 2012 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Aug 30 16:39:50 2012 +0200 @@ -176,7 +176,7 @@ local fun finish_thy ((thy, present, commit): result) = - (Global_Theory.join_proofs thy; Future.join present; commit (); thy); + (Thm.join_all_proofs thy; Future.join present; commit (); thy); val schedule_seq = Graph.schedule (fn deps => fn (_, task) =>