src/Pure/Isar/expression.ML
changeset 57926 59b2572e8e93
parent 57860 bcc243ea48e7
child 58956 a816aa3ff391
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Aug 13 12:59:27 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Aug 13 13:30:28 2014 +0200
     1.3 @@ -924,7 +924,7 @@
     1.4  fun subscribe_or_activate lthy =
     1.5    if Named_Target.is_theory lthy
     1.6    then Local_Theory.subscription
     1.7 -  else Local_Theory.activate;
     1.8 +  else Locale.activate_fragment;
     1.9  
    1.10  fun subscribe_locale_only lthy =
    1.11    let
    1.12 @@ -964,7 +964,7 @@
    1.13      (K Local_Theory.subscription) expression raw_eqns;
    1.14  
    1.15  fun ephemeral_interpretation x =
    1.16 -  gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;
    1.17 +  gen_local_theory_interpretation cert_interpretation (K Locale.activate_fragment) x;
    1.18  
    1.19  fun interpretation x =
    1.20    gen_local_theory_interpretation cert_interpretation subscribe_or_activate x;