1.1 --- a/src/Pure/General/sha1.ML	Thu Jul 24 10:22:34 2014 +0200
     1.2 +++ b/src/Pure/General/sha1.ML	Thu Jul 24 10:38:46 2014 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    eqtype digest
     1.5    val digest: string -> digest
     1.6    val rep: digest -> string
     1.7 +  val fake: string -> digest
     1.8  end;
     1.9  
    1.10  structure SHA1: SHA1 =
    1.11 @@ -136,4 +137,6 @@
    1.12  val digest = Digest o digest_string;
    1.13  fun rep (Digest s) = s;
    1.14  
    1.15 +val fake = Digest;
    1.16 +
    1.17  end;

     2.1 --- a/src/Pure/General/sha1.scala	Thu Jul 24 10:22:34 2014 +0200
     2.2 +++ b/src/Pure/General/sha1.scala	Thu Jul 24 10:38:46 2014 +0200
     2.3 @@ -65,5 +65,7 @@
     2.4    def digest(bytes: Bytes): Digest = bytes.sha1_digest
     2.5  
     2.6    def digest(string: String): Digest = digest(Bytes(string))
     2.7 +
     2.8 +  def fake(rep: String): Digest = new Digest(rep)
     2.9  }
    2.10  

     3.1 --- a/src/Pure/General/sha1_polyml.ML	Thu Jul 24 10:22:34 2014 +0200
     3.2 +++ b/src/Pure/General/sha1_polyml.ML	Thu Jul 24 10:38:46 2014 +0200
     3.3 @@ -46,4 +46,6 @@
     3.4  val digest = Digest o digest_string;
     3.5  fun rep (Digest s) = s;
     3.6  
     3.7 +val fake = Digest;
     3.8 +
     3.9  end;

     4.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 24 10:22:34 2014 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 24 10:38:46 2014 +0200
     4.3 @@ -296,12 +296,7 @@
     4.4  
     4.5  fun define_blob digest text =
     4.6    map_state (fn (versions, blobs, commands, execution) =>
     4.7 -    let
     4.8 -      val sha1_digest = SHA1.digest text;
     4.9 -      val _ =
    4.10 -        digest = SHA1.rep sha1_digest orelse
    4.11 -          error ("Ill-defined blob: bad SHA1 digest " ^ digest ^ " vs. " ^ SHA1.rep sha1_digest);
    4.12 -      val blobs' = Symtab.update (digest, (sha1_digest, split_lines text)) blobs;
    4.13 +    let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs
    4.14      in (versions, blobs', commands, execution) end);
    4.15  
    4.16  fun the_blob (State {blobs, ...}) digest =