changeset 55801 | 28b59620f0d0 |
parent 55783 | da0513d95155 |
child 56208 | 06cc31dff138 |
--- a/src/Pure/System/session.scala Fri Feb 28 11:50:54 2014 +0100 +++ b/src/Pure/System/session.scala Fri Feb 28 11:58:26 2014 +0100 @@ -378,7 +378,7 @@ digest <- command.blobs_digests if !global_state().defined_blob(digest) } { - doc_blobs.retrieve(digest) match { + doc_blobs.get(digest) match { case Some(blob) => global_state >> (_.define_blob(digest)) prover.get.define_blob(blob)