src/Pure/proofterm.ML
changeset 41699 21492e1c2b5a
parent 41698 90597e044e5f
child 43278 1fbdcebb364b
     1.1 --- a/src/Pure/proofterm.ML	Thu Feb 03 19:21:12 2011 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Thu Feb 03 19:27:04 2011 +0100
     1.3 @@ -1455,7 +1455,7 @@
     1.4  
     1.5      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     1.6      val (i, body') =
     1.7 -      (* FIXME non-deterministic!? depends on fulfilled proof*)
     1.8 +      (*non-deterministic, depends on unknown promises*)
     1.9        (case strip_combt (fst (strip_combP prf)) of
    1.10          (PThm (i, ((old_name, prop', NONE), body')), args') =>
    1.11            if (old_name = "" orelse old_name = name) andalso prop1 = prop' andalso args = args'