src/Pure/Isar/interpretation.ML
changeset 68852 becaeaa334ae
parent 68851 6c9825c1e26b
child 68854 404e04f649d4
     1.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 13:38:52 2018 +0200
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:10:39 2018 +0200
     1.3 @@ -153,16 +153,11 @@
     1.4      (fn witss => fn eqns => Proof.map_context (after_qed witss eqns) #> Proof.reset_facts)
     1.5      "interpret" propss eqns goal_ctxt state;
     1.6  
     1.7 -fun add_registration registration ctxt = ctxt
     1.8 -  |> Proof_Context.set_stmt false
     1.9 -  |> Context.proof_map (Locale.add_registration registration)
    1.10 -  |> Proof_Context.restore_stmt ctxt;
    1.11 -
    1.12  fun gen_interpret prep_interpretation expression state =
    1.13    Proof.assert_forward_or_chain state
    1.14    |> Proof.context_of
    1.15    |> generic_interpretation prep_interpretation (setup_proof state)
    1.16 -    Attrib.local_notes add_registration expression [];
    1.17 +    Attrib.local_notes Locale.add_registration_proof expression [];
    1.18  
    1.19  in
    1.20