1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Dec 10 17:19:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Dec 11 18:30:26 2008 +0100
     1.3 @@ -24,13 +24,20 @@
     1.4  
     1.5  (* new locales *)
     1.6  
     1.7 -fun locale_extern x = if !new_locales then NewLocale.extern x else Locale.extern x;
     1.8 -fun locale_add_type_syntax x = if !new_locales then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
     1.9 -fun locale_add_term_syntax x = if !new_locales then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.10 -fun locale_add_declaration x = if !new_locales then NewLocale.add_declaration x else Locale.add_declaration x;
    1.11 -fun locale_add_thmss x = if !new_locales then NewLocale.add_thmss x else Locale.add_thmss x;
    1.12 -fun locale_init x = if !new_locales then NewLocale.init x else Locale.init x;
    1.13 -fun locale_intern x = if !new_locales then NewLocale.intern x else Locale.intern x;
    1.14 +fun locale_extern is_class x = 
    1.15 +  if !new_locales andalso not is_class then NewLocale.extern x else Locale.extern x;
    1.16 +fun locale_add_type_syntax is_class x =
    1.17 +  if !new_locales andalso not is_class then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
    1.18 +fun locale_add_term_syntax is_class x =
    1.19 +  if !new_locales andalso not is_class then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
    1.20 +fun locale_add_declaration is_class x =
    1.21 +  if !new_locales andalso not is_class then NewLocale.add_declaration x else Locale.add_declaration x;
    1.22 +fun locale_add_thmss is_class x =
    1.23 +  if !new_locales andalso not is_class then NewLocale.add_thmss x else Locale.add_thmss x;
    1.24 +fun locale_init x =
    1.25 +  if !new_locales then NewLocale.init x else Locale.init x;
    1.26 +fun locale_intern is_class x =
    1.27 +  if !new_locales andalso not is_class then NewLocale.intern x else Locale.intern x;
    1.28  
    1.29  (* context data *)
    1.30  
    1.31 @@ -58,7 +65,7 @@
    1.32  fun pretty_thy ctxt target is_locale is_class =
    1.33    let
    1.34      val thy = ProofContext.theory_of ctxt;
    1.35 -    val target_name = (if is_class then "class " else "locale ") ^ locale_extern thy target;
    1.36 +    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
    1.37      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.38        (#1 (ProofContext.inferred_fixes ctxt));
    1.39      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.40 @@ -94,7 +101,7 @@
    1.41        |> LocalTheory.target (Context.proof_map d0)
    1.42      else
    1.43        lthy
    1.44 -      |> LocalTheory.target (add target d')
    1.45 +      |> LocalTheory.target (add is_class target d')
    1.46    end;
    1.47  
    1.48  val type_syntax = target_decl locale_add_type_syntax;
    1.49 @@ -179,7 +186,7 @@
    1.50          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    1.51          #> Sign.restore_naming thy)
    1.52      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.53 -    |> is_locale ? LocalTheory.target (locale_add_thmss target kind target_facts)
    1.54 +    |> is_locale ? LocalTheory.target (locale_add_thmss is_class target kind target_facts)
    1.55      |> note_local kind local_facts
    1.56    end;
    1.57  
    1.58 @@ -367,7 +374,8 @@
    1.59  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
    1.60  
    1.61  fun context "-" thy = init NONE thy
    1.62 -  | context target thy = init (SOME (locale_intern thy target)) thy;
    1.63 +  | context target thy = init (SOME (locale_intern
    1.64 +      (not (NewLocale.test_locale thy (NewLocale.intern thy target))) thy target)) thy;
    1.65  
    1.66  fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
    1.67