# HG changeset patch
# User wenzelm
# Date 1273774559 -7200
# Node ID 49d3cc859a12e44c01676ca62a79fe168bc1f6b2
# Parent  201a4afd8533d4655505bbbcdd1dc1264e6deda9
avoid redundant rebinding of name/prop -- probably introduced accidentally in 80bb72a0f577;

diff -r 201a4afd8533 -r 49d3cc859a12 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu May 13 18:47:07 2010 +0200
+++ b/src/Pure/proofterm.ML	Thu May 13 20:15:59 2010 +0200
@@ -1421,12 +1421,12 @@
       else MinProof;
     val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
-    val (i, name, prop, body') =
+    fun new_prf () = (serial (), fulfill_proof_future thy promises body0);
+    val (i, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>
           if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args'
-          then (i, name, prop, body')
+          then (i, body')
           else new_prf ()
       | _ => new_prf ());
     val head = PThm (i, ((name, prop, NONE), body'));