future_proof: protect conclusion of deferred proof state;
authorwenzelm
Wed Oct 01 18:16:14 2008 +0200 (2008-10-01)
changeset 28450504c4edead13
parent 28449 b6c57eb0fc39
child 28451 0586b855c2b5
future_proof: protect conclusion of deferred proof state;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Wed Oct 01 18:16:10 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Wed Oct 01 18:16:14 2008 +0200
     1.3 @@ -996,13 +996,15 @@
     1.4      val (goal_ctxt, (_, goal)) = find_goal state;
     1.5      val {statement as (kind, propss, cprop), messages, using, goal, before_qed, after_qed} = goal;
     1.6      val prop = Thm.term_of cprop;
     1.7 +    val cprop_protected = #2 (Thm.dest_implies (Thm.cprop_of goal));
     1.8  
     1.9 -    val statement' = (kind, [[], [prop]], cprop);
    1.10 -    fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [th]);
    1.11 +    val statement' = (kind, [[], [Thm.term_of cprop_protected]], cprop_protected);
    1.12 +    val goal' = Thm.adjust_maxidx_thm ~1 (Drule.protectI RS Goal.init cprop_protected);
    1.13 +    fun after_qed' [[th]] = ProofContext.put_thms false (AutoBind.thisN, SOME [Goal.conclude th]);
    1.14      val this_name = ProofContext.full_name (ProofContext.reset_naming goal_ctxt) AutoBind.thisN;
    1.15  
    1.16      fun make_result () = state
    1.17 -      |> map_goal I (K (statement', messages, using, goal, before_qed, (#1 after_qed, after_qed')))
    1.18 +      |> map_goal I (K (statement', messages, using, goal', before_qed, (#1 after_qed, after_qed')))
    1.19        |> make_proof
    1.20        |> (fn result_ctxt => ProofContext.get_fact_single result_ctxt (Facts.named this_name));
    1.21      val finished_goal = Goal.protect (Goal.future_result goal_ctxt make_result prop);