# HG changeset patch
# User wenzelm
# Date 1332072262 -3600
# Node ID 421760a1efe726f161d18b47a7918c312146d084
# Parent  6f00d8a83eb7285d51be3d364555d9f85fd1f4bb
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global);
prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output);
simplified signatures;

diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/General/name_space.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -34,7 +34,6 @@
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
-  val default_naming: naming
   val conceal: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -46,14 +45,18 @@
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
   val qualified_path: bool -> binding -> naming -> naming
+  val default_naming: naming
+  val local_naming: naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val alias: naming -> binding -> string -> T -> T
-  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
+  val naming_of: Context.generic -> naming
+  val map_naming: (naming -> naming) -> Context.generic -> Context.generic
+  val declare: Context.generic -> bool -> binding -> T -> string * T
   type 'a table = T * 'a Symtab.table
-  val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
+  val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
   val get: 'a table -> string -> 'a
-  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
+  val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
@@ -240,7 +243,7 @@
 
 
 
-(** naming contexts **)
+(** naming context **)
 
 (* datatype naming *)
 
@@ -260,8 +263,6 @@
   (conceal, group, theory_name, f path));
 
 
-val default_naming = make_naming (false, NONE, "", []);
-
 val conceal = map_naming (fn (_, group, theory_name, path) =>
   (true, group, theory_name, path));
 
@@ -285,6 +286,9 @@
 fun qualified_path mandatory binding = map_path (fn path =>
   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
 
+val default_naming = make_naming (false, NONE, "", []);
+val local_naming = default_naming |> add_path "local";
+
 
 (* full name *)
 
@@ -348,6 +352,28 @@
 
 
 
+(** context naming **)
+
+structure Data_Args =
+struct
+  type T = naming;
+  val empty = default_naming;
+  fun extend _ = default_naming;
+  fun merge _ = default_naming;
+  fun init _ = local_naming;
+end;
+
+structure Global_Naming = Theory_Data(Data_Args);
+structure Local_Naming = Proof_Data(Data_Args);
+
+fun naming_of (Context.Theory thy) = Global_Naming.get thy
+  | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;
+
+fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)
+  | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);
+
+
+
 (** entry definition **)
 
 (* declaration *)
@@ -361,8 +387,9 @@
             err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
     in (kind, internals, entries') end);
 
-fun declare ctxt strict naming binding space =
+fun declare context strict binding space =
   let
+    val naming = naming_of context;
     val Naming {group, theory_name, ...} = naming;
     val (concealed, spec) = name_spec naming binding;
     val (accs, accs') = accesses naming binding;
@@ -380,7 +407,9 @@
     val space' = space
       |> fold (add_name name) accs
       |> new_entry strict (name, (accs', entry));
-    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
+    val _ =
+      Context_Position.report_generic context pos
+        (entry_markup true (kind_of space) (name, entry));
   in (name, space') end;
 
 
@@ -388,10 +417,10 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun check ctxt (space, tab) (xname, pos) =
+fun check context (space, tab) (xname, pos) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
-      SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
+      SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
     | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
   end;
 
@@ -400,8 +429,8 @@
     SOME x => x
   | NONE => error (undefined (kind_of space) name));
 
-fun define ctxt strict naming (binding, x) (space, tab) =
-  let val (name, space') = declare ctxt strict naming binding space
+fun define context strict (binding, x) (space, tab) =
+  let val (name, space') = declare context strict binding space
   in (name, (space', Symtab.update (name, x) tab)) end;
 
 fun empty_table kind = (empty kind, Symtab.empty);
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -92,9 +92,7 @@
   end;
 
 fun add_attribute name att comment thy = thy
-  |> Attributes.map
-    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
-      (name, (att, comment)) #> snd);
+  |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
 
 
 (* name space *)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/class.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -282,7 +282,7 @@
               | _ => NONE)
           | NONE => NONE)
       | NONE => NONE);
-    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
+    fun subst (c, _) = Option.map snd (AList.lookup (op =) operations c);
     val unchecks = these_unchecks thy sort;
   in
     ctxt
@@ -470,7 +470,7 @@
               fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
       | matchings _ = I;
     val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
-      handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
     val inst = map_type_tvar
       (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
@@ -522,7 +522,7 @@
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     val algebra = Sign.classes_of thy
-      |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
+      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -163,7 +163,7 @@
 );
 
 val intern = Name_Space.intern o #1 o Locales.get;
-fun check thy = #1 o Name_Space.check (Proof_Context.init_global thy) (Locales.get thy);
+fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
@@ -175,7 +175,7 @@
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
-  thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
+  thy |> Locales.map (Name_Space.define (Context.Theory thy) true
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/method.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -326,9 +326,7 @@
   end;
 
 fun add_method name meth comment thy = thy
-  |> Methods.map
-    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
-      (name, (meth, comment)) #> snd);
+  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
 
 
 (* get methods *)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -165,7 +165,7 @@
 
 val init_context =
   Proof_Context.set_stmt true #>
-  Proof_Context.map_naming (K Proof_Context.local_naming);
+  Proof_Context.map_naming (K Name_Space.local_naming);
 
 fun init ctxt =
   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -21,11 +21,6 @@
   val restore_mode: Proof.context -> Proof.context -> Proof.context
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
-  val local_naming: Name_Space.naming
-  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
-  val naming_of: Proof.context -> Name_Space.naming
-  val restore_naming: Proof.context -> Proof.context -> Proof.context
-  val full_name: Proof.context -> binding -> string
   val syntax_of: Proof.context -> Local_Syntax.T
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
@@ -37,6 +32,10 @@
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val facts_of: Proof.context -> Facts.T
   val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
+  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
+  val naming_of: Proof.context -> Name_Space.naming
+  val restore_naming: Proof.context -> Proof.context -> Proof.context
+  val full_name: Proof.context -> binding -> string
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
   val const_space: Proof.context -> Name_Space.T
@@ -141,7 +140,6 @@
     Context.generic -> Context.generic
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val target_naming_of: Context.generic -> Name_Space.naming
   val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
@@ -192,24 +190,20 @@
 datatype data =
   Data of
    {mode: mode,                  (*inner syntax mode*)
-    naming: Name_Space.naming,   (*local naming conventions*)
     syntax: Local_Syntax.T,      (*local syntax*)
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts*)
     cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
 
-fun make_data (mode, naming, syntax, tsig, consts, facts, cases) =
-  Data {mode = mode, naming = naming, syntax = syntax,
-    tsig = tsig, consts = consts, facts = facts, cases = cases};
-
-val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
+fun make_data (mode, syntax, tsig, consts, facts, cases) =
+  Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
 
 structure Data = Proof_Data
 (
   type T = data;
   fun init thy =
-    make_data (mode_default, local_naming, Local_Syntax.init thy,
+    make_data (mode_default, Local_Syntax.init thy,
       (Sign.tsig_of thy, Sign.tsig_of thy),
       (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
 );
@@ -217,39 +211,35 @@
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
 
 fun map_data f =
-  Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} =>
-    make_data (f (mode, naming, syntax, tsig, consts, facts, cases)));
+  Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} =>
+    make_data (f (mode, syntax, tsig, consts, facts, cases)));
 
-fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) =>
-  (mode, naming, syntax, tsig, consts, facts, cases));
+fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
+  (mode, syntax, tsig, consts, facts, cases));
 
 fun map_mode f =
-  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
-    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
-
-fun map_naming f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, f naming, syntax, tsig, consts, facts, cases));
+  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
+    (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
 
 fun map_syntax f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, naming, f syntax, tsig, consts, facts, cases));
+  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+    (mode, f syntax, tsig, consts, facts, cases));
 
 fun map_tsig f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, naming, syntax, f tsig, consts, facts, cases));
+  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+    (mode, syntax, f tsig, consts, facts, cases));
 
 fun map_consts f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, naming, syntax, tsig, f consts, facts, cases));
+  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+    (mode, syntax, tsig, f consts, facts, cases));
 
 fun map_facts f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, naming, syntax, tsig, consts, f facts, cases));
+  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+    (mode, syntax, tsig, consts, f facts, cases));
 
 fun map_cases f =
-  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
-    (mode, naming, syntax, tsig, consts, facts, f cases));
+  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
+    (mode, syntax, tsig, consts, facts, f cases));
 
 val get_mode = #mode o rep_data;
 val restore_mode = set_mode o get_mode;
@@ -258,10 +248,6 @@
 fun set_stmt stmt =
   map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
 
-val naming_of = #naming o rep_data;
-val restore_naming = map_naming o K o naming_of
-val full_name = Name_Space.full_name o naming_of;
-
 val syntax_of = #syntax o rep_data;
 val syn_of = Local_Syntax.syn_of o syntax_of;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
@@ -278,6 +264,15 @@
 val cases_of = #cases o rep_data;
 
 
+(* naming *)
+
+val naming_of = Name_Space.naming_of o Context.Proof;
+val map_naming = Context.proof_map o Name_Space.map_naming;
+val restore_naming = map_naming o K o naming_of;
+
+val full_name = Name_Space.full_name o naming_of;
+
+
 (* name spaces *)
 
 val class_space = Type.class_space o tsig_of;
@@ -300,7 +295,7 @@
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
+      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
@@ -495,12 +490,13 @@
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
+  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
 val read_arity =
   prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
+
 val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
 
 end;
@@ -892,7 +888,7 @@
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
   | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
+      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
 
 in
 
@@ -908,7 +904,7 @@
   in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
 
 fun put_thms do_props thms ctxt = ctxt
-  |> map_naming (K local_naming)
+  |> map_naming (K Name_Space.local_naming)
   |> Context_Position.set_visible false
   |> update_thms do_props (apfst Binding.name thms)
   |> Context_Position.restore_visible ctxt
@@ -993,11 +989,6 @@
 end;
 
 
-(* naming *)
-
-val target_naming_of = Context.cases Sign.naming_of naming_of;
-
-
 (* aliases *)
 
 fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
@@ -1020,7 +1011,7 @@
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
-      |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
+      |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Isar/typedecl.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -41,7 +41,7 @@
   end;
 
 fun basic_typedecl (b, n, mx) lthy =
-  basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
+  basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
     (b, n, mx) lthy;
 
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -109,9 +109,7 @@
 );
 
 fun add_antiq name scan thy = thy
-  |> Antiq_Parsers.map
-    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
-      (name, scan) #> snd);
+  |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
 
 val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
 val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
@@ -120,7 +118,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val ((xname, _), pos) = Args.dest_src src;
-    val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
+    val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
   in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
 
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -89,17 +89,11 @@
       Name_Space.merge_tables (options1, options2));
 );
 
-fun add_command name cmd thy =
-  thy |> Antiquotations.map
-    (apfst
-      (Name_Space.define
-        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
+fun add_command name cmd thy = thy
+  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
 
-fun add_option name opt thy =
-  thy |> Antiquotations.map
-    (apsnd
-      (Name_Space.define
-        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
+fun add_option name opt thy = thy
+  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
 
 val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
 val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
@@ -111,7 +105,7 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     val ((xname, _), pos) = Args.dest_src src;
-    val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
+    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
   in
     f src state ctxt handle ERROR msg =>
       cat_error msg ("The error(s) above occurred in document antiquotation: " ^
@@ -121,7 +115,7 @@
 fun option ((xname, pos), s) ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
+    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
   in opt s ctxt end;
 
 fun print_antiquotations ctxt =
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/consts.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -29,10 +29,9 @@
   val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
+  val declare: Context.generic -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
-    binding * term -> T -> (term * term) * T
+  val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
@@ -232,12 +231,12 @@
 
 (* declarations *)
 
-fun declare ctxt naming (b, declT) =
+fun declare context (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
       val _ = Binding.check b;
-      val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
+      val (_, decls') = decls |> Name_Space.define context true (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
 
@@ -268,9 +267,9 @@
 
 in
 
-fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
+fun abbreviate context tsig mode (b, raw_rhs) consts =
   let
-    val pp = Context.pretty ctxt;
+    val pp = Context.pretty_generic context;
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = Print_Mode.internal;
@@ -284,7 +283,7 @@
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
-    val lhs = Const (Name_Space.full_name naming b, T);
+    val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T);
   in
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
@@ -292,7 +291,7 @@
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val _ = Binding.check b;
         val (_, decls') = decls
-          |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
+          |> Name_Space.define context true (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> update_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/context.ML
--- a/src/Pure/context.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/context.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -76,6 +76,7 @@
   (*pretty printing context*)
   val pretty: Proof.context -> pretty
   val pretty_global: theory -> pretty
+  val pretty_generic: generic -> pretty
   val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
   (*thread data*)
   val thread_data: unit -> generic option
@@ -557,8 +558,9 @@
 
 exception PRETTY of generic;
 
-val pretty = Pretty o PRETTY o Proof;
-val pretty_global = Pretty o PRETTY o Theory;
+val pretty_generic = Pretty o PRETTY;
+val pretty = pretty_generic o Proof;
+val pretty_global = pretty_generic o Theory;
 
 fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/context_position.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -12,6 +12,7 @@
   val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
   val is_visible_proof: Context.generic -> bool
   val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
+  val report_generic: Context.generic -> Position.T -> Markup.T -> unit
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
@@ -33,6 +34,11 @@
 
 fun if_visible_proof context f x = if is_visible_proof context then f x else ();
 
+fun report_generic context pos markup =
+  if Config.get_generic context visible then
+    Output.report (Position.reported_text pos markup "")
+  else ();
+
 fun reported_text ctxt pos markup txt =
   if is_visible ctxt then Position.reported_text pos markup txt else "";
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/display.ML
--- a/src/Pure/display.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/display.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -185,7 +185,8 @@
     val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
     val defs = Theory.defs_of thy;
     val {restricts, reducts} = Defs.dest defs;
-    val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
+    val tsig = Sign.tsig_of thy;
+    val consts = Sign.consts_of thy;
     val {constants, constraints} = Consts.dest consts;
     val extern_const = Name_Space.extern ctxt (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/facts.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -32,10 +32,9 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
-  val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
-  val add_dynamic: Proof.context -> Name_Space.naming ->
-    binding * (Context.generic -> thm list) -> T -> string * T
+  val add_global: Context.generic -> binding * thm list -> T -> string * T
+  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
+  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
@@ -191,11 +190,11 @@
 
 local
 
-fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
+fun add context strict do_props (b, ths) (Facts {facts, props}) =
   let
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
-      else Name_Space.define ctxt strict naming (b, Static ths) facts;
+      else Name_Space.define context strict (b, Static ths) facts;
     val props' =
       if do_props
       then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
@@ -204,16 +203,16 @@
 
 in
 
-fun add_global ctxt = add ctxt true false;
-fun add_local ctxt = add ctxt false;
+fun add_global context = add context true false;
+fun add_local context = add context false;
 
 end;
 
 
 (* add dynamic entries *)
 
-fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
-  let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
+fun add_dynamic context (b, f) (Facts {facts, props}) =
+  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
   in (name, make_facts facts' props) end;
 
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/global_theory.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -156,13 +156,11 @@
   then app_att thms thy |-> register_proofs
   else
     let
-      val naming = Sign.naming_of thy;
-      val name = Name_Space.full_name naming b;
+      val name = Sign.full_name thy b;
       val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
       val thms'' = map (Thm.transfer thy') thms';
       val thy'' = thy'
-        |> (Data.map o apfst)
-            (Facts.add_global (Proof_Context.init_global thy') naming (b, thms'') #> snd);
+        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
     in (thms'', thy'') end;
 
 
@@ -196,8 +194,7 @@
 (* add_thms_dynamic *)
 
 fun add_thms_dynamic (b, f) thy = thy
-  |> (Data.map o apfst)
-      (Facts.add_dynamic (Proof_Context.init_global thy) (Sign.naming_of thy) (b, f) #> snd);
+  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
 
 
 (* note_thmss *)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/sign.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -7,17 +7,6 @@
 
 signature SIGN =
 sig
-  val rep_sg: theory ->
-   {naming: Name_Space.naming,
-    syn: Syntax.syntax,
-    tsig: Type.tsig,
-    consts: Consts.T}
-  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
-  val naming_of: theory -> Name_Space.naming
-  val full_name: theory -> binding -> string
-  val full_name_path: theory -> string -> binding -> string
-  val full_bname: theory -> bstring -> string
-  val full_bname_path: theory -> string -> bstring -> string
   val syn_of: theory -> Syntax.syntax
   val tsig_of: theory -> Type.tsig
   val classes_of: theory -> Sorts.algebra
@@ -42,6 +31,14 @@
   val the_const_type: theory -> string -> typ
   val declared_tyname: theory -> string -> bool
   val declared_const: theory -> string -> bool
+  val naming_of: theory -> Name_Space.naming
+  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
+  val restore_naming: theory -> theory -> theory
+  val inherit_naming: theory -> Proof.context -> Context.generic
+  val full_name: theory -> binding -> string
+  val full_name_path: theory -> string -> binding -> string
+  val full_bname: theory -> bstring -> string
+  val full_bname_path: theory -> string -> bstring -> string
   val const_monomorphic: theory -> string -> bool
   val const_typargs: theory -> string * typ -> typ list
   val const_instance: theory -> string * typ list -> typ
@@ -67,7 +64,7 @@
   val cert_prop: theory -> term -> term
   val no_frees: Proof.context -> term -> term
   val no_vars: Proof.context -> term -> term
-  val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
+  val add_type: Proof.context -> binding * int * mixfix -> theory -> theory
   val add_types_global: (binding * int * mixfix) list -> theory -> theory
   val add_nonterminals: Proof.context -> binding list -> theory -> theory
   val add_nonterminals_global: binding list -> theory -> theory
@@ -113,7 +110,6 @@
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
-  val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
   val hide_const: bool -> string -> theory -> theory
@@ -125,56 +121,37 @@
 (** datatype sign **)
 
 datatype sign = Sign of
- {naming: Name_Space.naming,    (*common naming conventions*)
-  syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
+ {syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   tsig: Type.tsig,              (*order-sorted signature of types*)
   consts: Consts.T};            (*polymorphic constants*)
 
-fun make_sign (naming, syn, tsig, consts) =
-  Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
+fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
 
 structure Data = Theory_Data_PP
 (
   type T = sign;
-  fun extend (Sign {syn, tsig, consts, ...}) =
-    make_sign (Name_Space.default_naming, syn, tsig, consts);
+  fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
 
-  val empty =
-    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
+  val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
 
   fun merge pp (sign1, sign2) =
     let
-      val ctxt = Syntax.init_pretty pp;
-      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
-      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
+      val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
+      val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
-      val naming = Name_Space.default_naming;
       val syn = Syntax.merge_syntax (syn1, syn2);
-      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
+      val tsig = Type.merge_tsig pp (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
-    in make_sign (naming, syn, tsig, consts) end;
+    in make_sign (syn, tsig, consts) end;
 );
 
 fun rep_sg thy = Data.get thy |> (fn Sign args => args);
 
-fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
-  make_sign (f (naming, syn, tsig, consts)));
-
-fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
-fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
-fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
-fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
-
+fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
 
-(* naming *)
-
-val naming_of = #naming o rep_sg;
-
-val full_name = Name_Space.full_name o naming_of;
-fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
-
-fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
-fun full_bname_path thy path = full_name_path thy path o Binding.name;
+fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
+fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
+fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
 
 
 (* syntax *)
@@ -222,6 +199,21 @@
 val declared_const = can o the_const_constraint;
 
 
+(* naming *)
+
+val naming_of = Name_Space.naming_of o Context.Theory;
+val map_naming = Context.theory_map o Name_Space.map_naming;
+val restore_naming = map_naming o K o naming_of;
+fun inherit_naming thy =
+  Context.Proof o Context.proof_map (Name_Space.map_naming (K (naming_of thy)));
+
+val full_name = Name_Space.full_name o naming_of;
+fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
+
+fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
+fun full_bname_path thy path = full_name_path thy path o Binding.name;
+
+
 
 (** name spaces **)
 
@@ -330,22 +322,21 @@
 
 (* add type constructors *)
 
-fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
+fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
   let
-    fun type_syntax (b, n, mx) =
-      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
-    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
-    val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
-  in (naming, syn', tsig', consts) end);
+    val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
+    val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
+    val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
+  in (syn', tsig', consts) end);
 
 fun add_types_global types thy =
-  add_types (Syntax.init_pretty_global thy) types thy;
+  fold (add_type (Syntax.init_pretty_global thy)) types thy;
 
 
 (* add nonterminals *)
 
-fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
-  (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
+fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) =>
+  (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts));
 
 fun add_nonterminals_global ns thy =
   add_nonterminals (Syntax.init_pretty_global thy) ns thy;
@@ -353,8 +344,8 @@
 
 (* add type abbreviations *)
 
-fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
-  (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
+fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) =>
+  (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts));
 
 
 (* modify syntax *)
@@ -409,7 +400,7 @@
     val args = map prep raw_args;
   in
     thy
-    |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
+    |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;
@@ -437,7 +428,7 @@
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
+      |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
@@ -458,18 +449,16 @@
 
 fun primitive_class (bclass, classes) thy =
   thy
-  |> map_sign (fn (naming, syn, tsig, consts) =>
-    let
-      val ctxt = Syntax.init_pretty_global thy;
-      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
-    in (naming, syn, tsig', consts) end)
+  |> map_sign (fn (syn, tsig, consts) =>
+      let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
+      in (syn, tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 fun primitive_classrel arg thy =
-  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
+  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
 
 fun primitive_arity arg thy =
-  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
+  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
 
 
 (* add translation functions *)
@@ -512,8 +501,6 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
-val restore_naming = map_naming o K o naming_of;
-
 
 (* hide names *)
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/simplifier.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -171,7 +171,7 @@
 
 (* get simprocs *)
 
-fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ =
@@ -202,14 +202,12 @@
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
       let
-        val naming = Proof_Context.target_naming_of context;
         val b' = Morphism.binding phi b;
         val simproc' = transform_simproc phi simproc;
       in
         context
         |> Data.map (fn (ss, tab) =>
-          (ss addsimprocs [simproc'],
-            #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab)))
+          (ss addsimprocs [simproc'], #2 (Name_Space.define context true (b', simproc') tab)))
       end)
   end;
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/sorts.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -38,15 +38,15 @@
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
   val minimal_sorts: algebra -> sort list -> sort Ord_List.T
-  val add_class: Proof.context -> class * class list -> algebra -> algebra
-  val add_classrel: Proof.context -> class * class -> algebra -> algebra
-  val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
+  val add_class: Context.pretty -> class * class list -> algebra -> algebra
+  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
+  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
-  val merge_algebra: Proof.context -> algebra * algebra -> algebra
-  val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
+  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
+  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
-  val class_error: Proof.context -> class_error -> string
+  val class_error: Context.pretty -> class_error -> string
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort
@@ -187,16 +187,16 @@
 
 fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
 
-fun err_cyclic_classes ctxt css =
+fun err_cyclic_classes pp css =
   error (cat_lines (map (fn cs =>
-    "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
+    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
 
-fun add_class ctxt (c, cs) = map_classes (fn classes =>
+fun add_class pp (c, cs) = map_classes (fn classes =>
   let
     val classes' = classes |> Graph.new_node (c, serial ())
       handle Graph.DUP dup => err_dup_class dup;
     val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
-      handle Graph.CYCLES css => err_cyclic_classes ctxt css;
+      handle Graph.CYCLES css => err_cyclic_classes pp css;
   in classes'' end);
 
 
@@ -207,12 +207,14 @@
 fun for_classes _ NONE = ""
   | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
 
-fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
-  error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
-    Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
-    Syntax.string_of_arity ctxt (t, Ss', [c']));
+fun err_conflict pp t cc (c, Ss) (c', Ss') =
+  let val ctxt = Syntax.init_pretty pp in
+    error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
+      Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
+      Syntax.string_of_arity ctxt (t, Ss', [c']))
+  end;
 
-fun coregular ctxt algebra t (c, Ss) ars =
+fun coregular pp algebra t (c, Ss) ars =
   let
     fun conflict (c', Ss') =
       if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -222,62 +224,62 @@
       else NONE;
   in
     (case get_first conflict ars of
-      SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
+      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
     | NONE => (c, Ss) :: ars)
   end;
 
 fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
 
-fun insert ctxt algebra t (c, Ss) ars =
+fun insert pp algebra t (c, Ss) ars =
   (case AList.lookup (op =) ars c of
-    NONE => coregular ctxt algebra t (c, Ss) ars
+    NONE => coregular pp algebra t (c, Ss) ars
   | SOME Ss' =>
       if sorts_le algebra (Ss, Ss') then ars
       else if sorts_le algebra (Ss', Ss)
-      then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
-      else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
+      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+      else err_conflict pp t NONE (c, Ss) (c, Ss'));
 
 in
 
-fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
+fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
 
-fun insert_complete_ars ctxt algebra (t, ars) arities =
+fun insert_complete_ars pp algebra (t, ars) arities =
   let val ars' =
     Symtab.lookup_list arities t
-    |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
+    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
   in Symtab.update (t, ars') arities end;
 
-fun add_arities ctxt arg algebra =
-  algebra |> map_arities (insert_complete_ars ctxt algebra arg);
+fun add_arities pp arg algebra =
+  algebra |> map_arities (insert_complete_ars pp algebra arg);
 
-fun add_arities_table ctxt algebra =
-  Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
+fun add_arities_table pp algebra =
+  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
 
 end;
 
 
 (* classrel *)
 
-fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
   Symtab.empty
-  |> add_arities_table ctxt algebra arities);
+  |> add_arities_table pp algebra arities);
 
-fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
+fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
   classes |> Graph.add_edge_trans_acyclic rel
-    handle Graph.CYCLES css => err_cyclic_classes ctxt css);
+    handle Graph.CYCLES css => err_cyclic_classes pp css);
 
 
 (* empty and merge *)
 
 val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
 
-fun merge_algebra ctxt
+fun merge_algebra pp
    (Algebra {classes = classes1, arities = arities1},
     Algebra {classes = classes2, arities = arities2}) =
   let
     val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
       handle Graph.DUP c => err_dup_class c
-        | Graph.CYCLES css => err_cyclic_classes ctxt css;
+        | Graph.CYCLES css => err_cyclic_classes pp css;
     val algebra0 = make_algebra (classes', Symtab.empty);
     val arities' =
       (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -285,20 +287,20 @@
       | (true, false) =>  (*no completion*)
           (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
             if pointer_eq (ars1, ars2) then raise Symtab.SAME
-            else insert_ars ctxt algebra0 t ars2 ars1)
+            else insert_ars pp algebra0 t ars2 ars1)
       | (false, true) =>  (*unary completion*)
           Symtab.empty
-          |> add_arities_table ctxt algebra0 arities1
+          |> add_arities_table pp algebra0 arities1
       | (false, false) => (*binary completion*)
           Symtab.empty
-          |> add_arities_table ctxt algebra0 arities1
-          |> add_arities_table ctxt algebra0 arities2);
+          |> add_arities_table pp algebra0 arities1
+          |> add_arities_table pp algebra0 arities2);
   in make_algebra (classes', arities') end;
 
 
 (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
 
-fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
+fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
   let
     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
     fun restrict_arity t (c, Ss) =
@@ -310,7 +312,7 @@
       else NONE;
     val classes' = classes |> Graph.restrict P;
     val arities' = arities |> Symtab.map (map_filter o restrict_arity);
-  in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
+  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
 
 
 
@@ -323,13 +325,14 @@
   No_Arity of string * class |
   No_Subsort of sort * sort;
 
-fun class_error ctxt (No_Classrel (c1, c2)) =
-      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
-  | class_error ctxt (No_Arity (a, c)) =
-      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
-  | class_error ctxt (No_Subsort (S1, S2)) =
-      "Cannot derive subsort relation " ^
-        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
+fun class_error pp =
+  let val ctxt = Syntax.init_pretty pp in
+    fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+     | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+     | No_Subsort (S1, S2) =>
+        "Cannot derive subsort relation " ^
+          Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2
+  end;
 
 exception CLASS_ERROR of class_error;
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/theory.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -177,7 +177,7 @@
 fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   let
     val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
-    val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
+    val (_, axioms') = Name_Space.define (Sign.inherit_naming thy ctxt) true axm axioms;
   in axioms' end);
 
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/thm.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -1772,9 +1772,7 @@
 
 fun add_oracle (b, oracle) thy =
   let
-    val naming = Sign.naming_of thy;
-    val (name, tab') =
-      Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
+    val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
     val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/type.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -87,16 +87,16 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
+  val add_class: Context.generic -> binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
-  val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
-  val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
+  val add_type: Context.generic -> binding * int -> tsig -> tsig
+  val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
+  val add_nonterminal: Context.generic -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
-  val add_arity: Proof.context -> arity -> tsig -> tsig
-  val add_classrel: Proof.context -> class * class -> tsig -> tsig
-  val merge_tsig: Proof.context -> tsig * tsig -> tsig
+  val add_arity: Context.pretty -> arity -> tsig -> tsig
+  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
+  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
 end;
 
 structure Type: TYPE =
@@ -318,8 +318,9 @@
   | _ => error (undecl_type a));
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
-  | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
-      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
+  | arity_sorts pp (TSig {classes, ...}) a S =
+      Sorts.mg_domain (#2 classes) a S
+        handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
 
 
 
@@ -584,14 +585,14 @@
 
 (* classes *)
 
-fun add_class ctxt naming (c, cs) tsig =
+fun add_class context (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
       val _ = Binding.check c;
-      val (c', space') = space |> Name_Space.declare ctxt true naming c;
-      val classes' = classes |> Sorts.add_class ctxt (c', cs');
+      val (c', space') = space |> Name_Space.declare context true c;
+      val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
     in ((space', classes'), default, types) end);
 
 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -600,7 +601,7 @@
 
 (* arities *)
 
-fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   let
     val _ =
       (case lookup_type tsig t of
@@ -609,18 +610,18 @@
       | NONE => error (undecl_type t));
     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
       handle TYPE (msg, _, _) => error msg;
-    val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
+    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   in ((space, classes'), default, types) end);
 
 
 (* classrel *)
 
-fun add_classrel ctxt rel tsig =
+fun add_classrel pp rel tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val rel' = pairself (cert_class tsig) rel
         handle TYPE (msg, _, _) => error msg;
-      val classes' = classes |> Sorts.add_classrel ctxt rel';
+      val classes' = classes |> Sorts.add_classrel pp rel';
     in ((space, classes'), default, types) end);
 
 
@@ -634,8 +635,8 @@
 
 local
 
-fun new_decl ctxt naming (c, decl) types =
-  (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
+fun new_decl context (c, decl) types =
+  (Binding.check c; #2 (Name_Space.define context true (c, decl) types));
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
@@ -651,11 +652,11 @@
 
 in
 
-fun add_type ctxt naming (c, n) =
+fun add_type context (c, n) =
   if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
-  else map_types (new_decl ctxt naming (c, LogicalType n));
+  else map_types (new_decl context (c, LogicalType n));
 
-fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
+fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let
     fun err msg =
       cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
@@ -669,9 +670,9 @@
       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
         [] => []
       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-  in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
+  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
-fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
+fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
 
 end;
 
@@ -681,7 +682,7 @@
 
 (* merge type signatures *)
 
-fun merge_tsig ctxt (tsig1, tsig2) =
+fun merge_tsig pp (tsig1, tsig2) =
   let
     val (TSig {classes = (space1, classes1), default = default1, types = types1,
       log_types = _}) = tsig1;
@@ -689,7 +690,7 @@
       log_types = _}) = tsig2;
 
     val space' = Name_Space.merge (space1, space2);
-    val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
+    val classes' = Sorts.merge_algebra pp (classes1, classes2);
     val default' = Sorts.inter_sort classes' (default1, default2);
     val types' = Name_Space.merge_tables (types1, types2);
   in build_tsig ((space', classes'), default', types') end;
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Pure/variable.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -341,12 +341,14 @@
 fun new_fixed ((x, x'), pos) ctxt =
   if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
   else
-    ctxt
-    |> map_fixes
-      (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
-        Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
-    |> declare_fixed x
-    |> declare_constraints (Syntax.free x');
+    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
+      ctxt
+      |> map_fixes
+        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
+          Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
+      |> declare_fixed x
+      |> declare_constraints (Syntax.free x')
+  end;
 
 fun new_fixes names' xs xs' ps =
   map_names (K names') #>
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -431,7 +431,7 @@
       |> fold (ensure_fun thy arities eqngr) cs
       |> fold (ensure_rhs thy arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
-    val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
+    val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
     fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
diff -r 6f00d8a83eb7 -r 421760a1efe7 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Mar 18 12:51:44 2012 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sun Mar 18 13:04:22 2012 +0100
@@ -571,10 +571,9 @@
 
 fun not_wellsorted thy permissive some_thm ty sort e =
   let
-    val ctxt = Syntax.init_pretty_global thy;
-    val err_class = Sorts.class_error ctxt e;
+    val err_class = Sorts.class_error (Context.pretty_global thy) e;
     val err_typ =
-      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+      "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
         Syntax.string_of_sort_global thy sort;
   in
     translation_error thy permissive some_thm "Wellsortedness error"
@@ -1001,7 +1000,7 @@
 fun read_const_exprs thy =
   let
     fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
-      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
+      ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');