src/Pure/Isar/expression.ML
changeset 56723 a8f71445c265
parent 56057 ad6bd8030d88
child 56809 b60009672a65
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Apr 25 17:54:54 2014 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Apr 25 21:45:04 2014 +0200
     1.3 @@ -921,14 +921,9 @@
     1.4  
     1.5  (* second dimension: relation to underlying target *)
     1.6  
     1.7 -fun subscribe lthy =
     1.8 -  if Named_Target.is_theory lthy
     1.9 -  then Generic_Target.theory_registration
    1.10 -  else Generic_Target.locale_dependency (Named_Target.the_name lthy);
    1.11 -
    1.12  fun subscribe_or_activate lthy =
    1.13    if Named_Target.is_theory lthy
    1.14 -  then subscribe lthy
    1.15 +  then Local_Theory.subscription
    1.16    else Local_Theory.activate;
    1.17  
    1.18  fun subscribe_locale_only lthy =
    1.19 @@ -937,7 +932,7 @@
    1.20        if Named_Target.is_theory lthy
    1.21        then error "Not possible on level of global theory"
    1.22        else ();
    1.23 -  in subscribe lthy end;
    1.24 +  in Local_Theory.subscription end;
    1.25  
    1.26  
    1.27  (* special case: global sublocale command *)
    1.28 @@ -964,7 +959,7 @@
    1.29  fun interpret_cmd x = gen_interpret read_interpretation x;
    1.30  
    1.31  fun permanent_interpretation x =
    1.32 -  gen_local_theory_interpretation cert_interpretation subscribe x;
    1.33 +  gen_local_theory_interpretation cert_interpretation (K Local_Theory.subscription) x;
    1.34  
    1.35  fun ephemeral_interpretation x =
    1.36    gen_local_theory_interpretation cert_interpretation (K Local_Theory.activate) x;