tuned comments;
authorwenzelm
Thu Feb 03 19:27:04 2011 +0100 (2011-02-03 ago)
changeset 4169921492e1c2b5a
parent 41698 90597e044e5f
child 41700 f33d5a00c25d
tuned comments;
src/Pure/proofterm.ML
src/Pure/thm.ML
     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'
     2.1 --- a/src/Pure/thm.ML	Thu Feb 03 19:21:12 2011 +0100
     2.2 +++ b/src/Pure/thm.ML	Thu Feb 03 19:27:04 2011 +0100
     2.3 @@ -576,6 +576,7 @@
     2.4  
     2.5  (* closed derivations with official name *)
     2.6  
     2.7 +(*non-deterministic, depends on unknown promises*)
     2.8  fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
     2.9    Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);
    2.10