# HG changeset patch
# User wenzelm
# Date 1226961275 -3600
# Node ID 261bf00c6ede6d1527656cdc47d852e8d5058a48
# Parent  c67ab5df760b50c55dad19af22898bbc3370a89b
finish_proof: undefined promises may occur here;

diff -r c67ab5df760b -r 261bf00c6ede src/Pure/proofterm.ML
--- 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;