tuned;
authorwenzelm
Thu Aug 30 12:36:26 2018 +0200 (13 months ago)
changeset 688506d2735ca0271
parent 68849 0f9b2fa0556f
child 68851 6c9825c1e26b
tuned;
src/Pure/Isar/interpretation.ML
     1.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 12:10:15 2018 +0200
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 12:36:26 2018 +0200
     1.3 @@ -145,23 +145,21 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun setup_proof state after_qed propss eqns goal_ctxt =
     1.8 +  Element.witness_local_proof_eqs
     1.9 +    (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
    1.10 +    "interpret" propss eqns goal_ctxt state;
    1.11 +
    1.12 +fun add_registration reg mixin export ctxt = ctxt
    1.13 +  |> Proof_Context.set_stmt false
    1.14 +  |> Context.proof_map (Locale.add_registration reg mixin export)
    1.15 +  |> Proof_Context.restore_stmt ctxt;
    1.16 +
    1.17  fun gen_interpret prep_interpretation expression state =
    1.18 -  let
    1.19 -    val _ = Proof.assert_forward_or_chain state;
    1.20 -    fun lift_after_qed after_qed witss eqns =
    1.21 -      Proof.map_context (after_qed witss eqns) #> Proof.reset_facts;
    1.22 -    fun setup_proof after_qed propss eqns goal_ctxt =
    1.23 -      Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
    1.24 -        propss eqns goal_ctxt state;
    1.25 -    fun add_registration reg mixin export ctxt = ctxt
    1.26 -      |> Proof_Context.set_stmt false
    1.27 -      |> Context.proof_map (Locale.add_registration reg mixin export)
    1.28 -      |> Proof_Context.restore_stmt ctxt;
    1.29 -  in
    1.30 -    Proof.context_of state
    1.31 -    |> generic_interpretation prep_interpretation setup_proof
    1.32 -      Attrib.local_notes add_registration expression []
    1.33 -  end;
    1.34 +  Proof.assert_forward_or_chain state
    1.35 +  |> Proof.context_of
    1.36 +  |> generic_interpretation prep_interpretation (setup_proof state)
    1.37 +    Attrib.local_notes add_registration expression [];
    1.38  
    1.39  in
    1.40