1.1 --- a/src/Pure/Isar/ROOT.ML	Wed Nov 19 08:58:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/ROOT.ML	Wed Nov 19 16:58:33 2008 +0100
     1.3 @@ -51,6 +51,7 @@
     1.4  use "obtain.ML";
     1.5  
     1.6  (*local theories and targets*)
     1.7 +val new_locales = ref false;
     1.8  use "local_theory.ML";
     1.9  use "overloading.ML";
    1.10  use "locale.ML";

     2.1 --- a/src/Pure/Isar/theory_target.ML	Wed Nov 19 08:58:57 2008 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Nov 19 16:58:33 2008 +0100
     2.3 @@ -23,15 +23,13 @@
     2.4  
     2.5  (* new locales *)
     2.6  
     2.7 -val new_locales = false;
     2.8 -
     2.9 -fun locale_extern x = if new_locales then NewLocale.extern x else Locale.extern x;
    2.10 -fun locale_add_type_syntax x = if new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    2.11 -fun locale_add_term_syntax x = if new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    2.12 -fun locale_add_declaration x = if new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    2.13 -fun locale_add_thmss x = if new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    2.14 -fun locale_init x = if new_locales then NewLocale.init x else Locale.init x;
    2.15 -fun locale_intern x = if new_locales then NewLocale.intern x else Locale.intern x;
    2.16 +fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
    2.17 +fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    2.18 +fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    2.19 +fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    2.20 +fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    2.21 +fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
    2.22 +fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
    2.23  
    2.24  (* context data *)
    2.25