src/Pure/Isar/theory_target.ML
changeset 29249 4dc278c8dc59
parent 29228 40b3630b0deb
child 29252 ea97aa6aeba2
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Dec 19 15:05:37 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 19 16:39:23 2008 +0100
     1.3 @@ -25,19 +25,19 @@
     1.4  (* new locales *)
     1.5  
     1.6  fun locale_extern new_locale x = 
     1.7 -  if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
     1.8 +  if new_locale then NewLocale.extern x else Locale.extern x;
     1.9  fun locale_add_type_syntax new_locale x =
    1.10 -  if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.11 +  if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.12  fun locale_add_term_syntax new_locale x =
    1.13 -  if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.14 +  if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.15  fun locale_add_declaration new_locale x =
    1.16 -  if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
    1.17 +  if new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
    1.18  fun locale_add_thmss new_locale x =
    1.19 -  if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
    1.20 +  if new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
    1.21  fun locale_init new_locale x =
    1.22 -  if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
    1.23 +  if new_locale then NewLocale.init x else Locale.init x;
    1.24  fun locale_intern new_locale x =
    1.25 -  if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
    1.26 +  if new_locale then NewLocale.intern x else Locale.intern x;
    1.27  
    1.28  (* context data *)
    1.29