1.1 --- a/src/Pure/proofterm.ML	Thu May 13 18:47:07 2010 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Thu May 13 20:15:59 2010 +0200
     1.3 @@ -1421,12 +1421,12 @@
     1.4        else MinProof;
     1.5      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     1.6  
     1.7 -    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
     1.8 -    val (i, name, prop, body') =
     1.9 +    fun new_prf () = (serial (), fulfill_proof_future thy promises body0);
    1.10 +    val (i, body') =
    1.11        (case strip_combt (fst (strip_combP prf)) of
    1.12          (PThm (i, ((old_name, prop', NONE), body')), args') =>
    1.13            if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args'
    1.14 -          then (i, name, prop, body')
    1.15 +          then (i, body')
    1.16            else new_prf ()
    1.17        | _ => new_prf ());
    1.18      val head = PThm (i, ((name, prop, NONE), body'));