# HG changeset patch
# User ballarin
# Date 1227110313 -3600
# Node ID 9458d7a6388a39e04d13b88e7f8f5126a0d4f948
# Parent  9a02932efb91bfcd3034d4c2b393bf7346a6a8f2
Enable switching to new locales during session.

diff -r 9a02932efb91 -r 9458d7a6388a src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Wed Nov 19 08:58:57 2008 +0100
+++ b/src/Pure/Isar/ROOT.ML	Wed Nov 19 16:58:33 2008 +0100
@@ -51,6 +51,7 @@
 use "obtain.ML";
 
 (*local theories and targets*)
+val new_locales = ref false;
 use "local_theory.ML";
 use "overloading.ML";
 use "locale.ML";
diff -r 9a02932efb91 -r 9458d7a6388a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Nov 19 08:58:57 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Nov 19 16:58:33 2008 +0100
@@ -23,15 +23,13 @@
 
 (* new locales *)
 
-val new_locales = false;
-
-fun locale_extern x = if new_locales then NewLocale.extern x else Locale.extern x;
-fun locale_add_type_syntax x = if new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
-fun locale_add_term_syntax x = if new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
-fun locale_add_declaration x = if new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
-fun locale_add_thmss x = if new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
-fun locale_init x = if new_locales then NewLocale.init x else Locale.init x;
-fun locale_intern x = if new_locales then NewLocale.intern x else Locale.intern x;
+fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
+fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
+fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
+fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
+fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
 
 (* context data *)