author | wenzelm |
Tue, 31 Mar 2009 14:10:46 +0200 | |
changeset 30821 | 7d6d1f9a0b41 |
parent 30820 | a489921b77f4 (diff) |
parent 30818 | 17059c24014d (current diff) |
child 30822 | 8aac4b974280 |
child 30827 | fe4331fb3806 |
--- a/src/Pure/Thy/thy_info.ML Tue Mar 31 14:10:14 2009 +0200 +++ b/src/Pure/Thy/thy_info.ML Tue Mar 31 14:10:46 2009 +0200 @@ -371,7 +371,7 @@ val futures = fold fork tasks Symtab.empty; - val exns = rev tasks |> maps (fn (name, _) => + val exns = tasks |> maps (fn (name, _) => let val after_load = Future.join (the (Symtab.lookup futures name)); val proof_exns = join_thy name;