src/Pure/Isar/theory_target.ML

--- a/src/Pure/Isar/theory_target.ML	Wed Dec 10 17:19:25 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Dec 11 18:30:26 2008 +0100
@@ -24,13 +24,20 @@
 
 (* new locales *)
 
-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 is_class x = 
+  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
+fun locale_add_type_syntax is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+fun locale_add_term_syntax is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+fun locale_add_declaration is_class x =
+  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
+fun locale_add_thmss is_class x =
+  if !new_locales andalso not is_class 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 is_class x =
+  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
 
 (* context data *)
 
@@ -58,7 +65,7 @@
 fun pretty_thy ctxt target is_locale is_class =
   let
     val thy = ProofContext.theory_of ctxt;
-    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
+    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
     val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
       (#1 (ProofContext.inferred_fixes ctxt));
     val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
@@ -94,7 +101,7 @@
       |> LocalTheory.target (Context.proof_map d0)
     else
       lthy
-      |> LocalTheory.target (add target d')
+      |> LocalTheory.target (add is_class target d')
   end;
 
 val type_syntax = target_decl locale_add_type_syntax;
@@ -179,7 +186,7 @@
         #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
         #> Sign.restore_naming thy)
     |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
-    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
+    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
     |> note_local kind local_facts
   end;
 
@@ -367,7 +374,8 @@
 fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
 
 fun context "-" thy = init NONE thy
-  | context target thy = init (SOME (locale_intern thy target)) thy;
+  | context target thy = init (SOME (locale_intern
+      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);