Tuned function thm_proof.

--- a/src/Pure/proofterm.ML	Wed Oct 31 19:37:04 2001 +0100
+++ b/src/Pure/proofterm.ML	Wed Oct 31 19:41:29 2001 +0100
@@ -1031,7 +1031,7 @@
         #4 (shrink [] 0 (rewrite_prf fst (!(ProofData.get_sg sign))
           (foldr (uncurry implies_intr_proof) (hyps', prf))))
       else MinProof (mk_min_proof ([], prf));
-    val head = (case strip_combt (fst (strip_combP prf)) of
+    val head = (case strip_combt (fst (strip_combP opt_prf)) of
         (PThm ((old_name, _), prf', prop', None), args') =>
           if (old_name="" orelse old_name=name) andalso
              prop = prop' andalso args = args' then