src/Pure/Isar/expression.ML
changeset 56057 ad6bd8030d88
parent 55997 9dc5ce83202c
child 56723 a8f71445c265
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 11 22:49:28 2014 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 12 10:42:28 2014 +0100
     1.3 @@ -944,9 +944,16 @@
     1.4  
     1.5  fun gen_sublocale_global prep_loc prep_interpretation
     1.6      before_exit raw_locale expression raw_eqns thy =
     1.7 -  thy
     1.8 -  |> Named_Target.init before_exit (prep_loc thy raw_locale)
     1.9 -  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
    1.10 +  let
    1.11 +    val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
    1.12 +    fun setup_proof after_qed =
    1.13 +      Element.witness_proof_eqs
    1.14 +        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
    1.15 +  in
    1.16 +    lthy |>
    1.17 +      generic_interpretation prep_interpretation setup_proof
    1.18 +        Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
    1.19 +  end;
    1.20  
    1.21  in
    1.22