finish_proof: undefined promises may occur here;

--- a/src/Pure/proofterm.ML	Mon Nov 17 23:17:13 2008 +0100
+++ b/src/Pure/proofterm.ML	Mon Nov 17 23:34:35 2008 +0100
@@ -1218,7 +1218,7 @@
     val tab = Inttab.make promises;
     fun fill (Promise (i, prop, Ts)) =
         (case Inttab.lookup tab i of
-          NONE => error ("finish_proof: undefined promise " ^ string_of_int i)
+          NONE => NONE
         | SOME p => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) (Lazy.force p)))
       | fill _ = NONE;
     val (rules, procs) = get_data thy;