src/Pure/goal.ML
changeset 28363 c2432d193705
parent 28355 b9d9360e2440
child 28446 a01de3b3fa2e
     1.1 --- a/src/Pure/goal.ML	Thu Sep 25 20:34:17 2008 +0200
     1.2 +++ b/src/Pure/goal.ML	Thu Sep 25 20:34:18 2008 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4        Drule.implies_intr_list assms o
     1.5        Thm.adjust_maxidx_thm ~1 o result;
     1.6      val local_result =
     1.7 -      Thm.promise (Future.fork_irrelevant global_result) (cert global_prop)
     1.8 +      Thm.promise global_result (cert global_prop)
     1.9        |> Thm.instantiate (instT, [])
    1.10        |> Drule.forall_elim_list fixes
    1.11        |> fold (Thm.elim_implies o Thm.assume) assms;
    1.12 @@ -176,7 +176,7 @@
    1.13            end);
    1.14      val res =
    1.15        if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 then result ()
    1.16 -      else promise_result ctxt result (Thm.term_of stmt);
    1.17 +      else promise_result ctxt' result (Thm.term_of stmt);
    1.18    in
    1.19      Conjunction.elim_balanced (length props) res
    1.20      |> map (Assumption.export false ctxt' ctxt)