# HG changeset patch
# User wenzelm
# Date 1281543473 -7200
# Node ID ea1ee55aa41f49e163e2d51b3dcc83b8152d7614
# Parent  480b2de9927c76c8f45833bbbdb5cda650f37748# Parent  f6c1e169f51b36c1aded9594834ba7fb90acab2a
merged

diff -r f6c1e169f51b -r ea1ee55aa41f NEWS
--- a/NEWS	Wed Aug 11 18:11:07 2010 +0200
+++ b/NEWS	Wed Aug 11 18:17:53 2010 +0200
@@ -35,6 +35,10 @@
 
 *** HOL ***
 
+* Theory Library/Monad_Syntax provides do-syntax for monad types.  Syntax
+in Library/State_Monad has been changed to avoid ambiguities.
+INCOMPATIBILITY.
+
 * code generator: export_code without explicit file declaration prints
 to standard output.  INCOMPATIBILITY.
 
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Aug 11 18:17:53 2010 +0200
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
+      |> Class.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Wed Aug 11 18:17:53 2010 +0200
@@ -131,7 +131,11 @@
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
     == "CONST scomp t (\<lambda>p. e)"
   "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
-    == "CONST fcomp t e"
+    => "CONST fcomp t e"
+  "_sdo_final (_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e)))"
+    <= "_sdo_final (CONST fcomp t e)"
+  "_sdo_block (_sdo_cons (_sdo_then t) e)"
+    <= "CONST fcomp t (_sdo_block e)"
   "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
     == "let p = t in _sdo_block bs"
   "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -115,7 +115,7 @@
       #> snd
   in
     thy
-    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -145,7 +145,7 @@
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
-      ||> Theory_Target.instantiation
+      ||> Class.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -292,14 +292,14 @@
 
 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;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
-    val lthy = Theory_Target.overloading ops thy;
+    val lthy = Overloading.overloading ops 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 f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -86,7 +86,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in   
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
+    |> Class.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
@@ -304,7 +304,7 @@
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
     thy
-    |> Theory_Target.instantiation (tycos, vs, @{sort random})
+    |> Class.instantiation (tycos, vs, @{sort random})
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -116,7 +116,7 @@
     thy
     |> Code.add_datatype [constr]
     |> Code.add_eqn proj_constr
-    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
+    |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition
          (NONE, (Attrib.empty_binding, eq)))
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOL/Typerep.thy	Wed Aug 11 18:17:53 2010 +0200
@@ -56,7 +56,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
+    |> Class.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -203,7 +203,7 @@
     val below_eqn = Logic.mk_equals (below_const newT,
       Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
     val lthy3 = thy2
-      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
     val ((_, (_, below_ldef)), lthy4) = lthy3
       |> Specification.definition (NONE,
           ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
diff -r f6c1e169f51b -r ea1ee55aa41f src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -112,7 +112,7 @@
 
     (*instantiate class rep*)
     val lthy = thy
-      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep});
     val ((_, (_, emb_ldef)), lthy) =
         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
     val ((_, (_, prj_ldef)), lthy) =
diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/IsaMakefile	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -47,6 +47,8 @@
   val read_multi_arity: theory -> xstring list * xstring list * xstring
     -> string list * (string * sort) list * sort
   val type_name: string -> string
+  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
+  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
 
   (*subclasses*)
   val register_subclass: class * class -> morphism option -> Element.witness option
@@ -580,6 +582,35 @@
       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case instantiation_param lthy b
+   of SOME c => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
+            ##>> AxClass.define_overloaded b_def (c, rhs))
+          ||> confirm_declaration b
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun instantiation arities thy =
+  thy
+  |> init_instantiation arities
+  |> Local_Theory.init NONE ""
+     {define = Generic_Target.define instantiation_foundation,
+      notes = Generic_Target.notes
+        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+      abbrev = Generic_Target.abbrev
+        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+      declaration = K Generic_Target.theory_declaration,
+      syntax_declaration = K Generic_Target.theory_declaration,
+      pretty = single o pretty_instantiation,
+      reinit = instantiation arities o ProofContext.theory_of,
+      exit = Local_Theory.target_of o conclude_instantiation};
+
+fun instantiation_cmd arities thy =
+  instantiation (read_multi_arity thy arities) thy;
+
 
 (* simplified instantiation interface with no class parameter *)
 
diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -21,11 +21,21 @@
     -> term list -> local_theory -> local_theory)
     -> string * bool -> (binding * mixfix) * term -> local_theory
     -> (term * term) * local_theory
+
+  val theory_declaration: declaration -> local_theory -> local_theory
+  val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
+    -> term list * term list -> local_theory -> (term * thm) * local_theory
+  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
+    -> local_theory -> local_theory
+  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
+    -> local_theory -> local_theory
 end;
 
 structure Generic_Target: GENERIC_TARGET =
 struct
 
+(** lifting primitive to target operations **)
+
 (* mixfix syntax *)
 
 fun check_mixfix ctxt (b, extra_tfrees) mx =
@@ -176,4 +186,40 @@
     |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   end;
 
+
+(** primitive theory operations **)
+
+fun theory_declaration decl lthy =
+  let
+    val global_decl = Morphism.form
+      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
+  in
+    lthy
+    |> Local_Theory.theory (Context.theory_map global_decl)
+    |> Local_Theory.target (Context.proof_map global_decl)
+  end;
+
+fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  let
+    val (const, lthy2) = lthy |> Local_Theory.theory_result
+      (Sign.declare_const ((b, U), mx));
+    val lhs = list_comb (const, type_params @ term_params);
+    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
+      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
+  in ((lhs, def), lthy3) end;
+
+fun theory_notes kind global_facts lthy =
+  let
+    val thy = ProofContext.theory_of lthy;
+    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
+  in
+    lthy
+    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
+    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
+  end;
+
+fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
+  (Sign.add_abbrev (#1 prmode) (b, t) #->
+    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
+
 end;
diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 18:17:53 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 *)
@@ -472,7 +472,7 @@
   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
    (Parse.multi_arity --| Parse.begin
      >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
+         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
@@ -492,7 +492,7 @@
       Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
       >> Parse.triple1) --| Parse.begin
    >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
+         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 
 (* code generation *)
diff -r f6c1e169f51b -r ea1ee55aa41f 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 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -19,6 +19,9 @@
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
+
+  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
+  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;
 
 structure Overloading: OVERLOADING =
@@ -194,4 +197,40 @@
       (Pretty.str "overloading" :: map pr_operation overloading)
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case operation lthy b
+   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (declare (c, U)
+            ##>> define checked b_def (c, rhs))
+          ||> confirm b
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun gen_overloading prep_const raw_ops thy =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val ops = raw_ops |> map (fn (name, const, checked) =>
+      (name, Term.dest_Const (prep_const ctxt const), checked));
+  in
+    thy
+    |> init ops
+    |> Local_Theory.init NONE ""
+       {define = Generic_Target.define overloading_foundation,
+        notes = Generic_Target.notes
+          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        abbrev = Generic_Target.abbrev
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+            Generic_Target.theory_abbrev prmode ((b, mx), t)),
+        declaration = K Generic_Target.theory_declaration,
+        syntax_declaration = K Generic_Target.theory_declaration,
+        pretty = single o pretty,
+        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
+        exit = Local_Theory.target_of o conclude}
+  end;
+
+val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
+val overloading_cmd = gen_overloading Syntax.read_term;
+
 end;
diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 18:11:07 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,360 +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,
-    instantiation: string list * (string * sort) list * sort,
-    overloading: (string * (string * typ) * bool) list}
-  val init: string option -> theory -> local_theory
-  val context_cmd: xstring -> theory -> local_theory
-  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
-  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
-  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
-  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
-end;
-
-structure Theory_Target: THEORY_TARGET =
-struct
-
-(* context data *)
-
-datatype target = Target of {target: string, is_locale: bool,
-  is_class: bool, instantiation: string list * (string * sort) list * sort,
-  overloading: (string * (string * typ) * bool) list};
-
-fun make_target target is_locale is_class instantiation overloading =
-  Target {target = target, is_locale = is_locale,
-    is_class = is_class, instantiation = instantiation, overloading = overloading};
-
-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 theory_declaration decl lthy =
-  let
-    val global_decl = Morphism.form
-      (Morphism.transform (Local_Theory.global_morphism lthy) decl);
-  in
-    lthy
-    |> Local_Theory.theory (Context.theory_map global_decl)
-    |> Local_Theory.target (Context.proof_map global_decl)
-  end;
-
-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 ? theory_declaration decl
-    |> Local_Theory.target (add locale locale_decl)
-  end;
-
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
-  if target = "" then 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 syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
-fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  let
-    val (const, lthy2) = lthy |> Local_Theory.theory_result
-      (Sign.declare_const ((b, U), mx));
-    val lhs = list_comb (const, type_params @ term_params);
-    val ((_, def), lthy3) = lthy2 |> Local_Theory.theory_result
-      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
-  in ((lhs, def), lthy3) end;
-
-fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
-  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) =
-  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 instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case Class_Target.instantiation_param lthy b
-   of SOME c => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
-            ##>> AxClass.define_overloaded b_def (c, rhs))
-          ||> Class_Target.confirm_declaration b
-    | NONE => lthy |>
-        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case Overloading.operation lthy b
-   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
-            ##>> Overloading.define checked b_def (c, rhs))
-          ||> Overloading.confirm b
-    | NONE => lthy |>
-        theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
-fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
-  if not is_locale then (NoSyn, NoSyn, mx)
-  else if not is_class then (NoSyn, mx, NoSyn)
-  else (mx, NoSyn, NoSyn);
-
-fun foundation (ta as Target {target, is_locale, is_class, ...})
-    (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  let
-    val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    val (const, lthy2) = lthy |>
-      (case Class_Target.instantiation_param lthy b of
-        SOME c =>
-          if mx3 <> NoSyn then syntax_error c
-          else Local_Theory.theory_result (AxClass.declare_overloaded (c, U))
-            ##> Class_Target.confirm_declaration b
-      | NONE =>
-          (case Overloading.operation lthy b of
-            SOME (c, _) =>
-              if mx3 <> NoSyn then syntax_error c
-              else Local_Theory.theory_result (Overloading.declare (c, U))
-                ##> Overloading.confirm b
-          | NONE => Local_Theory.theory_result (Sign.declare_const ((b, U), mx3))));
-    val Const (head, _) = const;
-    val lhs = list_comb (const, type_params @ term_params);
-  in
-    lthy2
-    |> pair lhs
-    ||>> Local_Theory.theory_result
-      (case Overloading.operation lthy b of
-        SOME (_, checked) => Overloading.define checked b_def (head, rhs)
-      | NONE =>
-          if is_some (Class_Target.instantiation_param lthy b)
-          then AxClass.define_overloaded b_def (head, rhs)
-          else Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)) #>> snd)
-    ||> is_locale ? locale_const_declaration ta Syntax.mode_default ((b, mx2), lhs)
-    ||> is_class ? class_target ta
-          (Class_Target.declare target ((b, mx1), (type_params, lhs)))
-  end;
-
-
-(* notes *)
-
-fun theory_notes kind global_facts lthy =
-  let
-    val thy = ProofContext.theory_of lthy;
-    val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts;
-  in
-    lthy
-    |> Local_Theory.theory (PureThy.note_thmss kind global_facts' #> snd)
-    |> Local_Theory.target (ProofContext.note_thmss kind global_facts' #> snd)
-  end;
-
-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 _ => theory_notes kind global_facts;
-
-
-(* abbrev *)
-
-fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory
-  (Sign.add_abbrev (#1 prmode) (b, t) #->
-    (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)]));
-
-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
-      |> 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, instantiation, overloading, ...}) ctxt =
-  Pretty.block [Pretty.command "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
-    (if not (null overloading) then [Overloading.pretty ctxt]
-     else if not (null (#1 instantiation)) then [Class_Target.pretty_instantiation ctxt]
-     else pretty_thy ctxt target is_class);
-
-
-(* init various targets *)
-
-local
-
-fun init_data (Target {target, is_locale, is_class, instantiation, overloading}) =
-  if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
-  else if not (null overloading) then Overloading.init overloading
-  else 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, instantiation, overloading, ...}) thy =
-  thy
-  |> init_data ta
-  |> Data.put ta
-  |> Local_Theory.init NONE (Long_Name.base_name target)
-     {define = Generic_Target.define (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 o
-        (if not (null (#1 instantiation)) then Class_Target.conclude_instantiation
-         else if not (null overloading) then Overloading.conclude
-         else I)};
-
-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);
-
-fun gen_overloading prep_const raw_ops thy =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val ops = raw_ops |> map (fn (name, const, checked) =>
-      (name, Term.dest_Const (prep_const ctxt const), checked));
-  in
-    thy
-    |> Overloading.init ops
-    |> Local_Theory.init NONE ""
-       {define = Generic_Target.define overloading_foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
-        abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
-            theory_abbrev prmode ((b, mx), t)),
-        declaration = fn pervasive => theory_declaration,
-        syntax_declaration = fn pervasive => theory_declaration,
-        pretty = single o Overloading.pretty,
-        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
-        exit = Local_Theory.target_of o Overloading.conclude}
-  end;
-
-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;
-
-fun instantiation arities thy =
-  thy
-  |> Class_Target.init_instantiation arities
-  |> Local_Theory.init NONE ""
-     {define = Generic_Target.define instantiation_foundation,
-      notes = Generic_Target.notes
-        (fn kind => fn global_facts => fn _ => theory_notes kind global_facts),
-      abbrev = Generic_Target.abbrev
-        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => theory_abbrev prmode ((b, mx), t)),
-      declaration = fn pervasive => theory_declaration,
-      syntax_declaration = fn pervasive => theory_declaration,
-      pretty = single o Class_Target.pretty_instantiation,
-      reinit = instantiation arities o ProofContext.theory_of,
-      exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
-
-fun instantiation_cmd arities thy =
-  instantiation (Class_Target.read_multi_arity thy arities) thy;
-
-val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
-val overloading_cmd = gen_overloading Syntax.read_term;
-
-end;
-
-end;
diff -r f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -102,7 +102,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
@@ -191,7 +191,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 f6c1e169f51b -r ea1ee55aa41f src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Wed Aug 11 18:17:53 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 f6c1e169f51b -r ea1ee55aa41f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 11 18:17:53 2010 +0200
@@ -205,12 +205,12 @@
 
 (*local theories and targets*)
 use "Isar/local_theory.ML";
+use "Isar/locale.ML";
 use "Isar/generic_target.ML";
 use "Isar/overloading.ML";
-use "Isar/locale.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 f6c1e169f51b -r ea1ee55aa41f src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed Aug 11 18:11:07 2010 +0200
+++ b/src/Tools/quickcheck.ML	Wed Aug 11 18:17:53 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