# HG changeset patch
# User haftmann
# Date 1281530738 -7200
# Node ID 480b2de9927c76c8f45833bbbdb5cda650f37748
# Parent  ed50e21e715a7cd703fc3a48357aa87e3edb1b22
renamed Theory_Target to the more appropriate Named_Target

diff -r ed50e21e715a -r 480b2de9927c src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -348,7 +348,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Theory_Target.init name
+  |> Named_Target.init name
   |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
diff -r ed50e21e715a -r 480b2de9927c src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -998,7 +998,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> Theory_Target.init NONE
+      |> Named_Target.init NONE
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);
diff -r ed50e21e715a -r 480b2de9927c src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -292,7 +292,7 @@
 
 fun add_primrec_global fixes specs thy =
   let
-    val lthy = Theory_Target.init NONE thy;
+    val lthy = Named_Target.init NONE thy;
     val ((ts, simps), lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
diff -r ed50e21e715a -r 480b2de9927c src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -268,7 +268,7 @@
   in typedef_result inhabited lthy' end;
 
 fun add_typedef_global def opt_name typ set opt_morphs tac =
-  Theory_Target.init NONE
+  Named_Target.init NONE
   #> add_typedef def opt_name typ set opt_morphs tac
   #> Local_Theory.exit_result_global (apsnd o transform_info);
 
diff -r ed50e21e715a -r 480b2de9927c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/IsaMakefile	Wed Aug 11 14:45:38 2010 +0200
@@ -127,6 +127,7 @@
   Isar/local_theory.ML					\
   Isar/locale.ML					\
   Isar/method.ML					\
+  Isar/named_target.ML					\
   Isar/object_logic.ML					\
   Isar/obtain.ML					\
   Isar/outer_syntax.ML					\
@@ -144,7 +145,6 @@
   Isar/skip_proof.ML					\
   Isar/spec_rules.ML					\
   Isar/specification.ML					\
-  Isar/theory_target.ML					\
   Isar/token.ML						\
   Isar/toplevel.ML					\
   Isar/typedecl.ML					\
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -7,7 +7,7 @@
 signature CLASS =
 sig
   include CLASS_TARGET
-    (*FIXME the split into class_target.ML, theory_target.ML and
+    (*FIXME the split into class_target.ML, Named_Target.ML and
       class.ML is artificial*)
 
   val class: binding -> class list -> Element.context_i list
@@ -296,7 +296,7 @@
        Context.theory_map (Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> Theory_Target.init (SOME class)
+    |> Named_Target.init (SOME class)
     |> pair class
   end;
 
@@ -316,7 +316,7 @@
   let
     val thy = ProofContext.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case Theory_Target.peek lthy
+    val proto_sub = case Named_Target.peek lthy
      of {is_class = false, ...} => error "Not in a class context"
       | {target, ...} => target;
     val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
@@ -329,7 +329,7 @@
     fun after_qed some_wit =
       ProofContext.theory (register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
+      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -775,7 +775,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
-      |> Theory_Target.init (SOME name)
+      |> Named_Target.init (SOME name)
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -870,7 +870,7 @@
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = Theory_Target.init (SOME target) thy;
+    val target_ctxt = Named_Target.init (SOME target) thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -406,7 +406,7 @@
 val _ =
   Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
     (Parse.name --| Parse.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context_cmd name)));
+      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
 
 
 (* locales *)
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/named_target.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/named_target.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -0,0 +1,211 @@
+(*  Title:      Pure/Isar/theory_target.ML
+    Author:     Makarius
+    Author:     Florian Haftmann, TU Muenchen
+
+Targets for theory, locale and class.
+*)
+
+signature NAMED_TARGET =
+sig
+  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
+  val init: string option -> theory -> local_theory
+  val context_cmd: xstring -> theory -> local_theory
+end;
+
+structure Named_Target: NAMED_TARGET =
+struct
+
+(* context data *)
+
+datatype target = Target of {target: string, is_locale: bool, is_class: bool};
+
+fun make_target target is_locale is_class =
+  Target {target = target, is_locale = is_locale, is_class = is_class};
+
+val global_target = make_target "" false false;
+
+structure Data = Proof_Data
+(
+  type T = target;
+  fun init _ = global_target;
+);
+
+val peek = (fn Target args => args) o Data.get;
+
+
+(* generic declarations *)
+
+fun locale_declaration locale { syntax, pervasive } decl lthy =
+  let
+    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
+    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
+  in
+    lthy
+    |> pervasive ? Generic_Target.theory_declaration decl
+    |> Local_Theory.target (add locale locale_decl)
+  end;
+
+fun target_declaration (Target {target, ...}) { syntax, pervasive } =
+  if target = "" then Generic_Target.theory_declaration
+  else locale_declaration target { syntax = syntax, pervasive = pervasive };
+
+
+(* consts in locales *)
+
+fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
+  let
+    val b' = Morphism.binding phi b;
+    val rhs' = Morphism.term phi rhs;
+    val arg = (b', Term.close_schematic_term rhs');
+    val same_shape = Term.aconv_untyped (rhs, rhs');
+    (* FIXME workaround based on educated guess *)
+    val prefix' = Binding.prefix_of b';
+    val is_canonical_class = is_class andalso
+      (Binding.eq_name (b, b')
+        andalso not (null prefix')
+        andalso List.last prefix' = (Class_Target.class_prefix target, false)
+      orelse same_shape);
+  in
+    not is_canonical_class ?
+      (Context.mapping_result
+        (Sign.add_abbrev Print_Mode.internal arg)
+        (ProofContext.add_abbrev Print_Mode.internal arg)
+      #-> (fn (lhs' as Const (d, _), _) =>
+          same_shape ?
+            (Context.mapping
+              (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
+             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
+  end;
+
+fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
+  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
+
+fun class_target (Target {target, ...}) f =
+  Local_Theory.raw_theory f #>
+  Local_Theory.target (Class_Target.refresh_syntax target);
+
+
+(* define *)
+
+fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
+    #> pair (lhs, def))
+
+fun class_foundation (ta as Target {target, ...})
+    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
+  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
+  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
+    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
+    #> pair (lhs, def))
+
+fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
+  if is_class then class_foundation ta
+  else if is_locale then locale_foundation ta
+  else Generic_Target.theory_foundation;
+
+
+(* notes *)
+
+fun locale_notes locale kind global_facts local_facts lthy = 
+  let
+    val global_facts' = Attrib.map_facts (K I) global_facts;
+    val local_facts' = Element.facts_map
+      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
+  in
+    lthy
+    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
+  end
+
+fun target_notes (ta as Target {target, is_locale, ...}) =
+  if is_locale then locale_notes target
+    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+
+
+(* abbrev *)
+
+fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
+  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
+    (fn (lhs, _) => locale_const_declaration ta prmode
+      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
+
+fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
+    prmode (b, mx) (global_rhs, t') xs lthy =
+  if is_locale
+    then lthy
+      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
+      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
+    else lthy
+      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
+
+
+(* pretty *)
+
+fun pretty_thy ctxt target is_class =
+  let
+    val thy = ProofContext.theory_of ctxt;
+    val target_name =
+      [Pretty.command (if is_class then "class" else "locale"),
+        Pretty.str (" " ^ Locale.extern 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, [])]))
+      (Assumption.all_assms_of ctxt);
+    val elems =
+      (if null fixes then [] else [Element.Fixes fixes]) @
+      (if null assumes then [] else [Element.Assumes assumes]);
+  in
+    if target = "" then []
+    else if null elems then [Pretty.block target_name]
+    else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
+      map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
+  end;
+
+fun pretty (Target {target, is_class, ...}) ctxt =
+  Pretty.block [Pretty.command "theory", Pretty.brk 1,
+      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
+    pretty_thy ctxt target is_class;
+
+
+(* init various targets *)
+
+local
+
+fun init_data (Target {target, is_locale, is_class}) =
+  if not is_locale then ProofContext.init_global
+  else if not is_class then Locale.init target
+  else Class_Target.init target;
+
+fun init_target (ta as Target {target, ...}) thy =
+  thy
+  |> init_data ta
+  |> Data.put ta
+  |> Local_Theory.init NONE (Long_Name.base_name target)
+     {define = Generic_Target.define (target_foundation ta),
+      notes = Generic_Target.notes (target_notes ta),
+      abbrev = Generic_Target.abbrev (target_abbrev ta),
+      declaration = fn pervasive => target_declaration ta
+        { syntax = false, pervasive = pervasive },
+      syntax_declaration = fn pervasive => target_declaration ta
+        { syntax = true, pervasive = pervasive },
+      pretty = pretty ta,
+      reinit = init_target ta o ProofContext.theory_of,
+      exit = Local_Theory.target_of};
+
+fun named_target _ NONE = global_target
+  | named_target thy (SOME target) =
+      if Locale.defined thy target
+      then make_target target true (Class_Target.is_class thy target)
+      else error ("No such locale: " ^ quote target);
+
+in
+
+fun init target thy = init_target (named_target thy target) thy;
+
+fun context_cmd "-" thy = init NONE thy
+  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
+
+end;
+
+end;
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -185,7 +185,7 @@
 
     (*facts*)
     val (facts, facts_lthy) = axioms_thy
-      |> Theory_Target.init NONE
+      |> Named_Target.init NONE
       |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms)
       |> Local_Theory.notes axioms;
 
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:41:16 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-(*  Title:      Pure/Isar/theory_target.ML
-    Author:     Makarius
-    Author:     Florian Haftmann, TU Muenchen
-
-Common theory/locale/class/instantiation/overloading targets.
-*)
-
-signature THEORY_TARGET =
-sig
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
-  val init: string option -> theory -> local_theory
-  val context_cmd: xstring -> theory -> local_theory
-end;
-
-structure Theory_Target: THEORY_TARGET =
-struct
-
-(* context data *)
-
-datatype target = Target of {target: string, is_locale: bool, is_class: bool};
-
-fun make_target target is_locale is_class =
-  Target {target = target, is_locale = is_locale, is_class = is_class};
-
-val global_target = make_target "" false false;
-
-structure Data = Proof_Data
-(
-  type T = target;
-  fun init _ = global_target;
-);
-
-val peek = (fn Target args => args) o Data.get;
-
-
-(* generic declarations *)
-
-fun locale_declaration locale { syntax, pervasive } decl lthy =
-  let
-    val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
-    val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
-  in
-    lthy
-    |> pervasive ? Generic_Target.theory_declaration decl
-    |> Local_Theory.target (add locale locale_decl)
-  end;
-
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
-  if target = "" then Generic_Target.theory_declaration
-  else locale_declaration target { syntax = syntax, pervasive = pervasive };
-
-
-(* consts in locales *)
-
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
-  let
-    val b' = Morphism.binding phi b;
-    val rhs' = Morphism.term phi rhs;
-    val arg = (b', Term.close_schematic_term rhs');
-    val same_shape = Term.aconv_untyped (rhs, rhs');
-    (* FIXME workaround based on educated guess *)
-    val prefix' = Binding.prefix_of b';
-    val is_canonical_class = is_class andalso
-      (Binding.eq_name (b, b')
-        andalso not (null prefix')
-        andalso List.last prefix' = (Class_Target.class_prefix target, false)
-      orelse same_shape);
-  in
-    not is_canonical_class ?
-      (Context.mapping_result
-        (Sign.add_abbrev Print_Mode.internal arg)
-        (ProofContext.add_abbrev Print_Mode.internal arg)
-      #-> (fn (lhs' as Const (d, _), _) =>
-          same_shape ?
-            (Context.mapping
-              (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
-             Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
-  end;
-
-fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
-  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
-
-fun class_target (Target {target, ...}) f =
-  Local_Theory.raw_theory f #>
-  Local_Theory.target (Class_Target.refresh_syntax target);
-
-
-(* define *)
-
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
-    #> pair (lhs, def))
-
-fun class_foundation (ta as Target {target, ...})
-    (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
-    #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
-    #> pair (lhs, def))
-
-fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
-  if is_class then class_foundation ta
-  else if is_locale then locale_foundation ta
-  else Generic_Target.theory_foundation;
-
-
-(* notes *)
-
-fun locale_notes locale kind global_facts local_facts lthy = 
-  let
-    val global_facts' = Attrib.map_facts (K I) global_facts;
-    val local_facts' = Element.facts_map
-      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
-  in
-    lthy
-    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
-  end
-
-fun target_notes (ta as Target {target, is_locale, ...}) =
-  if is_locale then locale_notes target
-    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
-
-
-(* abbrev *)
-
-fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result
-  (Sign.add_abbrev Print_Mode.internal (b, t)) #->
-    (fn (lhs, _) => locale_const_declaration ta prmode
-      ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
-
-fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
-    prmode (b, mx) (global_rhs, t') xs lthy =
-  if is_locale
-    then lthy
-      |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs
-      |> is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx), t'))
-    else lthy
-      |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs);
-
-
-(* pretty *)
-
-fun pretty_thy ctxt target is_class =
-  let
-    val thy = ProofContext.theory_of ctxt;
-    val target_name =
-      [Pretty.command (if is_class then "class" else "locale"),
-        Pretty.str (" " ^ Locale.extern 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, [])]))
-      (Assumption.all_assms_of ctxt);
-    val elems =
-      (if null fixes then [] else [Element.Fixes fixes]) @
-      (if null assumes then [] else [Element.Assumes assumes]);
-  in
-    if target = "" then []
-    else if null elems then [Pretty.block target_name]
-    else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-      map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
-  end;
-
-fun pretty (Target {target, is_class, ...}) ctxt =
-  Pretty.block [Pretty.command "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
-    pretty_thy ctxt target is_class;
-
-
-(* init various targets *)
-
-local
-
-fun init_data (Target {target, is_locale, is_class}) =
-  if not is_locale then ProofContext.init_global
-  else if not is_class then Locale.init target
-  else Class_Target.init target;
-
-fun init_target (ta as Target {target, ...}) thy =
-  thy
-  |> init_data ta
-  |> Data.put ta
-  |> Local_Theory.init NONE (Long_Name.base_name target)
-     {define = Generic_Target.define (target_foundation ta),
-      notes = Generic_Target.notes (target_notes ta),
-      abbrev = Generic_Target.abbrev (target_abbrev ta),
-      declaration = fn pervasive => target_declaration ta
-        { syntax = false, pervasive = pervasive },
-      syntax_declaration = fn pervasive => target_declaration ta
-        { syntax = true, pervasive = pervasive },
-      pretty = pretty ta,
-      reinit = init_target ta o ProofContext.theory_of,
-      exit = Local_Theory.target_of};
-
-fun named_target _ NONE = global_target
-  | named_target thy (SOME target) =
-      if Locale.defined thy target
-      then make_target target true (Class_Target.is_class thy target)
-      else error ("No such locale: " ^ quote target);
-
-in
-
-fun init target thy = init_target (named_target thy target) thy;
-
-fun context_cmd "-" thy = init NONE thy
-  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
-
-end;
-
-end;
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -103,7 +103,7 @@
 
 (* local theory wrappers *)
 
-val loc_init = Theory_Target.context_cmd;
+val loc_init = Named_Target.context_cmd;
 val loc_exit = Local_Theory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -194,7 +194,7 @@
 
 (* print state *)
 
-val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I;
+val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I;
 
 fun print_state_context state =
   (case try node_of state of
diff -r ed50e21e715a -r 480b2de9927c src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -75,7 +75,7 @@
   end;
 
 fun typedecl_global decl =
-  Theory_Target.init NONE
+  Named_Target.init NONE
   #> typedecl decl
   #> Local_Theory.exit_result_global Morphism.typ;
 
@@ -115,7 +115,7 @@
 end;
 
 fun abbrev_global decl rhs =
-  Theory_Target.init NONE
+  Named_Target.init NONE
   #> abbrev decl rhs
   #> Local_Theory.exit_result_global (K I);
 
diff -r ed50e21e715a -r 480b2de9927c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -210,7 +210,7 @@
 use "Isar/overloading.ML";
 use "axclass.ML";
 use "Isar/class_target.ML";
-use "Isar/theory_target.ML";
+use "Isar/named_target.ML";
 use "Isar/expression.ML";
 use "Isar/class.ML";
 
diff -r ed50e21e715a -r 480b2de9927c src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Aug 11 14:41:16 2010 +0200
+++ b/src/Tools/quickcheck.ML	Wed Aug 11 14:45:38 2010 +0200
@@ -219,7 +219,7 @@
       | strip t = t;
     val {goal = st, ...} = Proof.raw_goal state;
     val (gi, frees) = Logic.goal_params (prop_of st) i;
-    val some_locale = case (#target o Theory_Target.peek) lthy
+    val some_locale = case (#target o Named_Target.peek) lthy
      of "" => NONE
       | locale => SOME locale;
     val assms = if no_assms then [] else case some_locale