src/Pure/Isar/interpretation.ML
changeset 67702 2d9918f5b33c
parent 67450 b0ae74b86ef3
child 67740 b6ce18784872
     1.1 --- a/src/Pure/Isar/interpretation.ML	Fri Feb 23 13:09:45 2018 +0100
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Fri Feb 23 14:12:48 2018 +0100
     1.3 @@ -175,10 +175,14 @@
     1.4      fun setup_proof after_qed propss eqns goal_ctxt =
     1.5        Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
     1.6          propss eqns goal_ctxt state;
     1.7 +    fun add_registration reg mixin export ctxt = ctxt
     1.8 +      |> Proof_Context.set_stmt false
     1.9 +      |> Context.proof_map (Locale.add_registration reg mixin export)
    1.10 +      |> Proof_Context.restore_stmt ctxt;
    1.11    in
    1.12      Proof.context_of state
    1.13      |> generic_interpretation prep_interpretation setup_proof
    1.14 -      Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
    1.15 +      Attrib.local_notes add_registration expression [] raw_eqns
    1.16    end;
    1.17  
    1.18  in