src/Pure/Isar/theory_target.ML
changeset 28849 9458d7a6388a
parent 28834 66d31ca2c5af
child 28861 f53abb0733ee
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Nov 19 08:58:57 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Nov 19 16:58:33 2008 +0100
     1.3 @@ -23,15 +23,13 @@
     1.4  
     1.5  (* new locales *)
     1.6  
     1.7 -val new_locales = false;
     1.8 -
     1.9 -fun locale_extern x = if new_locales then NewLocale.extern x else Locale.extern x;
    1.10 -fun locale_add_type_syntax x = if new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.11 -fun locale_add_term_syntax x = if new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.12 -fun locale_add_declaration x = if new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    1.13 -fun locale_add_thmss x = if new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    1.14 -fun locale_init x = if new_locales then NewLocale.init x else Locale.init x;
    1.15 -fun locale_intern x = if new_locales then NewLocale.intern x else Locale.intern x;
    1.16 +fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
    1.17 +fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.18 +fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.19 +fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    1.20 +fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    1.21 +fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
    1.22 +fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
    1.23  
    1.24  (* context data *)
    1.25