1.1 --- a/src/Pure/General/name_space.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -34,7 +34,6 @@
     1.4    val hide: bool -> string -> T -> T
     1.5    val merge: T * T -> T
     1.6    type naming
     1.7 -  val default_naming: naming
     1.8    val conceal: naming -> naming
     1.9    val get_group: naming -> serial option
    1.10    val set_group: serial option -> naming -> naming
    1.11 @@ -46,14 +45,18 @@
    1.12    val parent_path: naming -> naming
    1.13    val mandatory_path: string -> naming -> naming
    1.14    val qualified_path: bool -> binding -> naming -> naming
    1.15 +  val default_naming: naming
    1.16 +  val local_naming: naming
    1.17    val transform_binding: naming -> binding -> binding
    1.18    val full_name: naming -> binding -> string
    1.19    val alias: naming -> binding -> string -> T -> T
    1.20 -  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
    1.21 +  val naming_of: Context.generic -> naming
    1.22 +  val map_naming: (naming -> naming) -> Context.generic -> Context.generic
    1.23 +  val declare: Context.generic -> bool -> binding -> T -> string * T
    1.24    type 'a table = T * 'a Symtab.table
    1.25 -  val check: Proof.context -> 'a table -> xstring * Position.T -> string * 'a
    1.26 +  val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    1.27    val get: 'a table -> string -> 'a
    1.28 -  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    1.29 +  val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    1.30    val empty_table: string -> 'a table
    1.31    val merge_tables: 'a table * 'a table -> 'a table
    1.32    val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
    1.33 @@ -240,7 +243,7 @@
    1.34  
    1.35  
    1.36  
    1.37 -(** naming contexts **)
    1.38 +(** naming context **)
    1.39  
    1.40  (* datatype naming *)
    1.41  
    1.42 @@ -260,8 +263,6 @@
    1.43    (conceal, group, theory_name, f path));
    1.44  
    1.45  
    1.46 -val default_naming = make_naming (false, NONE, "", []);
    1.47 -
    1.48  val conceal = map_naming (fn (_, group, theory_name, path) =>
    1.49    (true, group, theory_name, path));
    1.50  
    1.51 @@ -285,6 +286,9 @@
    1.52  fun qualified_path mandatory binding = map_path (fn path =>
    1.53    path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
    1.54  
    1.55 +val default_naming = make_naming (false, NONE, "", []);
    1.56 +val local_naming = default_naming |> add_path "local";
    1.57 +
    1.58  
    1.59  (* full name *)
    1.60  
    1.61 @@ -348,6 +352,28 @@
    1.62  
    1.63  
    1.64  
    1.65 +(** context naming **)
    1.66 +
    1.67 +structure Data_Args =
    1.68 +struct
    1.69 +  type T = naming;
    1.70 +  val empty = default_naming;
    1.71 +  fun extend _ = default_naming;
    1.72 +  fun merge _ = default_naming;
    1.73 +  fun init _ = local_naming;
    1.74 +end;
    1.75 +
    1.76 +structure Global_Naming = Theory_Data(Data_Args);
    1.77 +structure Local_Naming = Proof_Data(Data_Args);
    1.78 +
    1.79 +fun naming_of (Context.Theory thy) = Global_Naming.get thy
    1.80 +  | naming_of (Context.Proof ctxt) = Local_Naming.get ctxt;
    1.81 +
    1.82 +fun map_naming f (Context.Theory thy) = Context.Theory (Global_Naming.map f thy)
    1.83 +  | map_naming f (Context.Proof ctxt) = Context.Proof (Local_Naming.map f ctxt);
    1.84 +
    1.85 +
    1.86 +
    1.87  (** entry definition **)
    1.88  
    1.89  (* declaration *)
    1.90 @@ -361,8 +387,9 @@
    1.91              err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
    1.92      in (kind, internals, entries') end);
    1.93  
    1.94 -fun declare ctxt strict naming binding space =
    1.95 +fun declare context strict binding space =
    1.96    let
    1.97 +    val naming = naming_of context;
    1.98      val Naming {group, theory_name, ...} = naming;
    1.99      val (concealed, spec) = name_spec naming binding;
   1.100      val (accs, accs') = accesses naming binding;
   1.101 @@ -380,7 +407,9 @@
   1.102      val space' = space
   1.103        |> fold (add_name name) accs
   1.104        |> new_entry strict (name, (accs', entry));
   1.105 -    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
   1.106 +    val _ =
   1.107 +      Context_Position.report_generic context pos
   1.108 +        (entry_markup true (kind_of space) (name, entry));
   1.109    in (name, space') end;
   1.110  
   1.111  
   1.112 @@ -388,10 +417,10 @@
   1.113  
   1.114  type 'a table = T * 'a Symtab.table;
   1.115  
   1.116 -fun check ctxt (space, tab) (xname, pos) =
   1.117 +fun check context (space, tab) (xname, pos) =
   1.118    let val name = intern space xname in
   1.119      (case Symtab.lookup tab name of
   1.120 -      SOME x => (Context_Position.report ctxt pos (markup space name); (name, x))
   1.121 +      SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
   1.122      | NONE => error (undefined (kind_of space) name ^ Position.str_of pos))
   1.123    end;
   1.124  
   1.125 @@ -400,8 +429,8 @@
   1.126      SOME x => x
   1.127    | NONE => error (undefined (kind_of space) name));
   1.128  
   1.129 -fun define ctxt strict naming (binding, x) (space, tab) =
   1.130 -  let val (name, space') = declare ctxt strict naming binding space
   1.131 +fun define context strict (binding, x) (space, tab) =
   1.132 +  let val (name, space') = declare context strict binding space
   1.133    in (name, (space', Symtab.update (name, x) tab)) end;
   1.134  
   1.135  fun empty_table kind = (empty kind, Symtab.empty);

     2.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 18 12:51:44 2012 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 18 13:04:22 2012 +0100
     2.3 @@ -92,9 +92,7 @@
     2.4    end;
     2.5  
     2.6  fun add_attribute name att comment thy = thy
     2.7 -  |> Attributes.map
     2.8 -    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
     2.9 -      (name, (att, comment)) #> snd);
    2.10 +  |> Attributes.map (Name_Space.define (Context.Theory thy) true (name, (att, comment)) #> snd);
    2.11  
    2.12  
    2.13  (* name space *)

     3.1 --- a/src/Pure/Isar/class.ML	Sun Mar 18 12:51:44 2012 +0100
     3.2 +++ b/src/Pure/Isar/class.ML	Sun Mar 18 13:04:22 2012 +0100
     3.3 @@ -282,7 +282,7 @@
     3.4                | _ => NONE)
     3.5            | NONE => NONE)
     3.6        | NONE => NONE);
     3.7 -    fun subst (c, ty) = Option.map snd (AList.lookup (op =) operations c);
     3.8 +    fun subst (c, _) = Option.map snd (AList.lookup (op =) operations c);
     3.9      val unchecks = these_unchecks thy sort;
    3.10    in
    3.11      ctxt
    3.12 @@ -470,7 +470,7 @@
    3.13                fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
    3.14        | matchings _ = I;
    3.15      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
    3.16 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error ctxt e);
    3.17 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
    3.18      val inst = map_type_tvar
    3.19        (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
    3.20    in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
    3.21 @@ -522,7 +522,7 @@
    3.22      val primary_constraints = map (apsnd
    3.23        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
    3.24      val algebra = Sign.classes_of thy
    3.25 -      |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
    3.26 +      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
    3.27              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    3.28      val consts = Sign.consts_of thy;
    3.29      val improve_constraints = AList.lookup (op =)

     4.1 --- a/src/Pure/Isar/locale.ML	Sun Mar 18 12:51:44 2012 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Sun Mar 18 13:04:22 2012 +0100
     4.3 @@ -163,7 +163,7 @@
     4.4  );
     4.5  
     4.6  val intern = Name_Space.intern o #1 o Locales.get;
     4.7 -fun check thy = #1 o Name_Space.check (Proof_Context.init_global thy) (Locales.get thy);
     4.8 +fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy);
     4.9  fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (#1 (Locales.get thy));
    4.10  
    4.11  val get_locale = Symtab.lookup o #2 o Locales.get;
    4.12 @@ -175,7 +175,7 @@
    4.13    | NONE => error ("Unknown locale " ^ quote name));
    4.14  
    4.15  fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
    4.16 -  thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    4.17 +  thy |> Locales.map (Name_Space.define (Context.Theory thy) true
    4.18      (binding,
    4.19        mk_locale ((parameters, spec, intros, axioms),
    4.20          ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),

     5.1 --- a/src/Pure/Isar/method.ML	Sun Mar 18 12:51:44 2012 +0100
     5.2 +++ b/src/Pure/Isar/method.ML	Sun Mar 18 13:04:22 2012 +0100
     5.3 @@ -326,9 +326,7 @@
     5.4    end;
     5.5  
     5.6  fun add_method name meth comment thy = thy
     5.7 -  |> Methods.map
     5.8 -    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
     5.9 -      (name, (meth, comment)) #> snd);
    5.10 +  |> Methods.map (Name_Space.define (Context.Theory thy) true (name, (meth, comment)) #> snd);
    5.11  
    5.12  
    5.13  (* get methods *)

     6.1 --- a/src/Pure/Isar/proof.ML	Sun Mar 18 12:51:44 2012 +0100
     6.2 +++ b/src/Pure/Isar/proof.ML	Sun Mar 18 13:04:22 2012 +0100
     6.3 @@ -165,7 +165,7 @@
     6.4  
     6.5  val init_context =
     6.6    Proof_Context.set_stmt true #>
     6.7 -  Proof_Context.map_naming (K Proof_Context.local_naming);
     6.8 +  Proof_Context.map_naming (K Name_Space.local_naming);
     6.9  
    6.10  fun init ctxt =
    6.11    State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));

     7.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 18 12:51:44 2012 +0100
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 18 13:04:22 2012 +0100
     7.3 @@ -21,11 +21,6 @@
     7.4    val restore_mode: Proof.context -> Proof.context -> Proof.context
     7.5    val abbrev_mode: Proof.context -> bool
     7.6    val set_stmt: bool -> Proof.context -> Proof.context
     7.7 -  val local_naming: Name_Space.naming
     7.8 -  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
     7.9 -  val naming_of: Proof.context -> Name_Space.naming
    7.10 -  val restore_naming: Proof.context -> Proof.context -> Proof.context
    7.11 -  val full_name: Proof.context -> binding -> string
    7.12    val syntax_of: Proof.context -> Local_Syntax.T
    7.13    val syn_of: Proof.context -> Syntax.syntax
    7.14    val tsig_of: Proof.context -> Type.tsig
    7.15 @@ -37,6 +32,10 @@
    7.16    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    7.17    val facts_of: Proof.context -> Facts.T
    7.18    val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
    7.19 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
    7.20 +  val naming_of: Proof.context -> Name_Space.naming
    7.21 +  val restore_naming: Proof.context -> Proof.context -> Proof.context
    7.22 +  val full_name: Proof.context -> binding -> string
    7.23    val class_space: Proof.context -> Name_Space.T
    7.24    val type_space: Proof.context -> Name_Space.T
    7.25    val const_space: Proof.context -> Name_Space.T
    7.26 @@ -141,7 +140,6 @@
    7.27      Context.generic -> Context.generic
    7.28    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
    7.29      Context.generic -> Context.generic
    7.30 -  val target_naming_of: Context.generic -> Name_Space.naming
    7.31    val class_alias: binding -> class -> Proof.context -> Proof.context
    7.32    val type_alias: binding -> string -> Proof.context -> Proof.context
    7.33    val const_alias: binding -> string -> Proof.context -> Proof.context
    7.34 @@ -192,24 +190,20 @@
    7.35  datatype data =
    7.36    Data of
    7.37     {mode: mode,                  (*inner syntax mode*)
    7.38 -    naming: Name_Space.naming,   (*local naming conventions*)
    7.39      syntax: Local_Syntax.T,      (*local syntax*)
    7.40      tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    7.41      consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    7.42      facts: Facts.T,              (*local facts*)
    7.43      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    7.44  
    7.45 -fun make_data (mode, naming, syntax, tsig, consts, facts, cases) =
    7.46 -  Data {mode = mode, naming = naming, syntax = syntax,
    7.47 -    tsig = tsig, consts = consts, facts = facts, cases = cases};
    7.48 -
    7.49 -val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    7.50 +fun make_data (mode, syntax, tsig, consts, facts, cases) =
    7.51 +  Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
    7.52  
    7.53  structure Data = Proof_Data
    7.54  (
    7.55    type T = data;
    7.56    fun init thy =
    7.57 -    make_data (mode_default, local_naming, Local_Syntax.init thy,
    7.58 +    make_data (mode_default, Local_Syntax.init thy,
    7.59        (Sign.tsig_of thy, Sign.tsig_of thy),
    7.60        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    7.61  );
    7.62 @@ -217,39 +211,35 @@
    7.63  fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
    7.64  
    7.65  fun map_data f =
    7.66 -  Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} =>
    7.67 -    make_data (f (mode, naming, syntax, tsig, consts, facts, cases)));
    7.68 +  Data.map (fn Data {mode, syntax, tsig, consts, facts, cases} =>
    7.69 +    make_data (f (mode, syntax, tsig, consts, facts, cases)));
    7.70  
    7.71 -fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) =>
    7.72 -  (mode, naming, syntax, tsig, consts, facts, cases));
    7.73 +fun set_mode mode = map_data (fn (_, syntax, tsig, consts, facts, cases) =>
    7.74 +  (mode, syntax, tsig, consts, facts, cases));
    7.75  
    7.76  fun map_mode f =
    7.77 -  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
    7.78 -    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
    7.79 -
    7.80 -fun map_naming f =
    7.81 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    7.82 -    (mode, f naming, syntax, tsig, consts, facts, cases));
    7.83 +  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, syntax, tsig, consts, facts, cases) =>
    7.84 +    (make_mode (f (stmt, pattern, schematic, abbrev)), syntax, tsig, consts, facts, cases));
    7.85  
    7.86  fun map_syntax f =
    7.87 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    7.88 -    (mode, naming, f syntax, tsig, consts, facts, cases));
    7.89 +  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
    7.90 +    (mode, f syntax, tsig, consts, facts, cases));
    7.91  
    7.92  fun map_tsig f =
    7.93 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    7.94 -    (mode, naming, syntax, f tsig, consts, facts, cases));
    7.95 +  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
    7.96 +    (mode, syntax, f tsig, consts, facts, cases));
    7.97  
    7.98  fun map_consts f =
    7.99 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
   7.100 -    (mode, naming, syntax, tsig, f consts, facts, cases));
   7.101 +  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
   7.102 +    (mode, syntax, tsig, f consts, facts, cases));
   7.103  
   7.104  fun map_facts f =
   7.105 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
   7.106 -    (mode, naming, syntax, tsig, consts, f facts, cases));
   7.107 +  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
   7.108 +    (mode, syntax, tsig, consts, f facts, cases));
   7.109  
   7.110  fun map_cases f =
   7.111 -  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
   7.112 -    (mode, naming, syntax, tsig, consts, facts, f cases));
   7.113 +  map_data (fn (mode, syntax, tsig, consts, facts, cases) =>
   7.114 +    (mode, syntax, tsig, consts, facts, f cases));
   7.115  
   7.116  val get_mode = #mode o rep_data;
   7.117  val restore_mode = set_mode o get_mode;
   7.118 @@ -258,10 +248,6 @@
   7.119  fun set_stmt stmt =
   7.120    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
   7.121  
   7.122 -val naming_of = #naming o rep_data;
   7.123 -val restore_naming = map_naming o K o naming_of
   7.124 -val full_name = Name_Space.full_name o naming_of;
   7.125 -
   7.126  val syntax_of = #syntax o rep_data;
   7.127  val syn_of = Local_Syntax.syn_of o syntax_of;
   7.128  val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
   7.129 @@ -278,6 +264,15 @@
   7.130  val cases_of = #cases o rep_data;
   7.131  
   7.132  
   7.133 +(* naming *)
   7.134 +
   7.135 +val naming_of = Name_Space.naming_of o Context.Proof;
   7.136 +val map_naming = Context.proof_map o Name_Space.map_naming;
   7.137 +val restore_naming = map_naming o K o naming_of;
   7.138 +
   7.139 +val full_name = Name_Space.full_name o naming_of;
   7.140 +
   7.141 +
   7.142  (* name spaces *)
   7.143  
   7.144  val class_space = Type.class_space o tsig_of;
   7.145 @@ -300,7 +295,7 @@
   7.146    map_tsig (fn tsig as (local_tsig, global_tsig) =>
   7.147      let val thy_tsig = Sign.tsig_of thy in
   7.148        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
   7.149 -      else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
   7.150 +      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)
   7.151      end) |>
   7.152    map_consts (fn consts as (local_consts, global_consts) =>
   7.153      let val thy_consts = Sign.consts_of thy in
   7.154 @@ -495,12 +490,13 @@
   7.155  
   7.156  fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   7.157    let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
   7.158 -  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
   7.159 +  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
   7.160  
   7.161  in
   7.162  
   7.163  val read_arity =
   7.164    prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
   7.165 +
   7.166  val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
   7.167  
   7.168  end;
   7.169 @@ -892,7 +888,7 @@
   7.170  
   7.171  fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
   7.172    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
   7.173 -      (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
   7.174 +      (Facts.add_local (Context.Proof ctxt) do_props (b, ths) #> snd);
   7.175  
   7.176  in
   7.177  
   7.178 @@ -908,7 +904,7 @@
   7.179    in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
   7.180  
   7.181  fun put_thms do_props thms ctxt = ctxt
   7.182 -  |> map_naming (K local_naming)
   7.183 +  |> map_naming (K Name_Space.local_naming)
   7.184    |> Context_Position.set_visible false
   7.185    |> update_thms do_props (apfst Binding.name thms)
   7.186    |> Context_Position.restore_visible ctxt
   7.187 @@ -993,11 +989,6 @@
   7.188  end;
   7.189  
   7.190  
   7.191 -(* naming *)
   7.192 -
   7.193 -val target_naming_of = Context.cases Sign.naming_of naming_of;
   7.194 -
   7.195 -
   7.196  (* aliases *)
   7.197  
   7.198  fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
   7.199 @@ -1020,7 +1011,7 @@
   7.200        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
   7.201      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   7.202      val ((lhs, rhs), consts') = consts_of ctxt
   7.203 -      |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
   7.204 +      |> Consts.abbreviate (Context.Proof ctxt) (tsig_of ctxt) mode (b, t);
   7.205    in
   7.206      ctxt
   7.207      |> (map_consts o apfst) (K consts')

     8.1 --- a/src/Pure/Isar/typedecl.ML	Sun Mar 18 12:51:44 2012 +0100
     8.2 +++ b/src/Pure/Isar/typedecl.ML	Sun Mar 18 13:04:22 2012 +0100
     8.3 @@ -41,7 +41,7 @@
     8.4    end;
     8.5  
     8.6  fun basic_typedecl (b, n, mx) lthy =
     8.7 -  basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
     8.8 +  basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
     8.9      (b, n, mx) lthy;
    8.10  
    8.11  

     9.1 --- a/src/Pure/ML/ml_context.ML	Sun Mar 18 12:51:44 2012 +0100
     9.2 +++ b/src/Pure/ML/ml_context.ML	Sun Mar 18 13:04:22 2012 +0100
     9.3 @@ -109,9 +109,7 @@
     9.4  );
     9.5  
     9.6  fun add_antiq name scan thy = thy
     9.7 -  |> Antiq_Parsers.map
     9.8 -    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
     9.9 -      (name, scan) #> snd);
    9.10 +  |> Antiq_Parsers.map (Name_Space.define (Context.Theory thy) true (name, scan) #> snd);
    9.11  
    9.12  val intern_antiq = Name_Space.intern o #1 o Antiq_Parsers.get;
    9.13  val defined_antiq = Symtab.defined o #2 o Antiq_Parsers.get;
    9.14 @@ -120,7 +118,7 @@
    9.15    let
    9.16      val thy = Proof_Context.theory_of ctxt;
    9.17      val ((xname, _), pos) = Args.dest_src src;
    9.18 -    val (_, scan) = Name_Space.check ctxt (Antiq_Parsers.get thy) (xname, pos);
    9.19 +    val (_, scan) = Name_Space.check (Context.Proof ctxt) (Antiq_Parsers.get thy) (xname, pos);
    9.20    in Args.context_syntax Isabelle_Markup.ML_antiquotationN (scan pos) src ctxt end;
    9.21  
    9.22  

    10.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 18 12:51:44 2012 +0100
    10.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 18 13:04:22 2012 +0100
    10.3 @@ -89,17 +89,11 @@
    10.4        Name_Space.merge_tables (options1, options2));
    10.5  );
    10.6  
    10.7 -fun add_command name cmd thy =
    10.8 -  thy |> Antiquotations.map
    10.9 -    (apfst
   10.10 -      (Name_Space.define
   10.11 -        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, cmd) #> snd));
   10.12 +fun add_command name cmd thy = thy
   10.13 +  |> Antiquotations.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> snd));
   10.14  
   10.15 -fun add_option name opt thy =
   10.16 -  thy |> Antiquotations.map
   10.17 -    (apsnd
   10.18 -      (Name_Space.define
   10.19 -        (Proof_Context.init_global thy) true (Sign.naming_of thy) (name, opt) #> snd));
   10.20 +fun add_option name opt thy = thy
   10.21 +  |> Antiquotations.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> snd));
   10.22  
   10.23  val intern_command = Name_Space.intern o #1 o #1 o Antiquotations.get;
   10.24  val defined_command = Symtab.defined o #2 o #1 o Antiquotations.get;
   10.25 @@ -111,7 +105,7 @@
   10.26    let
   10.27      val thy = Proof_Context.theory_of ctxt;
   10.28      val ((xname, _), pos) = Args.dest_src src;
   10.29 -    val (name, f) = Name_Space.check ctxt (#1 (Antiquotations.get thy)) (xname, pos);
   10.30 +    val (name, f) = Name_Space.check (Context.Proof ctxt) (#1 (Antiquotations.get thy)) (xname, pos);
   10.31    in
   10.32      f src state ctxt handle ERROR msg =>
   10.33        cat_error msg ("The error(s) above occurred in document antiquotation: " ^
   10.34 @@ -121,7 +115,7 @@
   10.35  fun option ((xname, pos), s) ctxt =
   10.36    let
   10.37      val thy = Proof_Context.theory_of ctxt;
   10.38 -    val (_, opt) = Name_Space.check ctxt (#2 (Antiquotations.get thy)) (xname, pos);
   10.39 +    val (_, opt) = Name_Space.check (Context.Proof ctxt) (#2 (Antiquotations.get thy)) (xname, pos);
   10.40    in opt s ctxt end;
   10.41  
   10.42  fun print_antiquotations ctxt =

    11.1 --- a/src/Pure/consts.ML	Sun Mar 18 12:51:44 2012 +0100
    11.2 +++ b/src/Pure/consts.ML	Sun Mar 18 13:04:22 2012 +0100
    11.3 @@ -29,10 +29,9 @@
    11.4    val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    11.5    val typargs: T -> string * typ -> typ list
    11.6    val instance: T -> string * typ list -> typ
    11.7 -  val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
    11.8 +  val declare: Context.generic -> binding * typ -> T -> T
    11.9    val constrain: string * typ option -> T -> T
   11.10 -  val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
   11.11 -    binding * term -> T -> (term * term) * T
   11.12 +  val abbreviate: Context.generic -> Type.tsig -> string -> binding * term -> T -> (term * term) * T
   11.13    val revert_abbrev: string -> string -> T -> T
   11.14    val hide: bool -> string -> T -> T
   11.15    val empty: T
   11.16 @@ -232,12 +231,12 @@
   11.17  
   11.18  (* declarations *)
   11.19  
   11.20 -fun declare ctxt naming (b, declT) =
   11.21 +fun declare context (b, declT) =
   11.22    map_consts (fn (decls, constraints, rev_abbrevs) =>
   11.23      let
   11.24        val decl = {T = declT, typargs = typargs_of declT};
   11.25        val _ = Binding.check b;
   11.26 -      val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
   11.27 +      val (_, decls') = decls |> Name_Space.define context true (b, (decl, NONE));
   11.28      in (decls', constraints, rev_abbrevs) end);
   11.29  
   11.30  
   11.31 @@ -268,9 +267,9 @@
   11.32  
   11.33  in
   11.34  
   11.35 -fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   11.36 +fun abbreviate context tsig mode (b, raw_rhs) consts =
   11.37    let
   11.38 -    val pp = Context.pretty ctxt;
   11.39 +    val pp = Context.pretty_generic context;
   11.40      val cert_term = certify pp tsig false consts;
   11.41      val expand_term = certify pp tsig true consts;
   11.42      val force_expand = mode = Print_Mode.internal;
   11.43 @@ -284,7 +283,7 @@
   11.44        |> Term.close_schematic_term;
   11.45      val normal_rhs = expand_term rhs;
   11.46      val T = Term.fastype_of rhs;
   11.47 -    val lhs = Const (Name_Space.full_name naming b, T);
   11.48 +    val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T);
   11.49    in
   11.50      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
   11.51        let
   11.52 @@ -292,7 +291,7 @@
   11.53          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
   11.54          val _ = Binding.check b;
   11.55          val (_, decls') = decls
   11.56 -          |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
   11.57 +          |> Name_Space.define context true (b, (decl, SOME abbr));
   11.58          val rev_abbrevs' = rev_abbrevs
   11.59            |> update_abbrevs mode (rev_abbrev lhs rhs);
   11.60        in (decls', constraints, rev_abbrevs') end)

    12.1 --- a/src/Pure/context.ML	Sun Mar 18 12:51:44 2012 +0100
    12.2 +++ b/src/Pure/context.ML	Sun Mar 18 13:04:22 2012 +0100
    12.3 @@ -76,6 +76,7 @@
    12.4    (*pretty printing context*)
    12.5    val pretty: Proof.context -> pretty
    12.6    val pretty_global: theory -> pretty
    12.7 +  val pretty_generic: generic -> pretty
    12.8    val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    12.9    (*thread data*)
   12.10    val thread_data: unit -> generic option
   12.11 @@ -557,8 +558,9 @@
   12.12  
   12.13  exception PRETTY of generic;
   12.14  
   12.15 -val pretty = Pretty o PRETTY o Proof;
   12.16 -val pretty_global = Pretty o PRETTY o Theory;
   12.17 +val pretty_generic = Pretty o PRETTY;
   12.18 +val pretty = pretty_generic o Proof;
   12.19 +val pretty_global = pretty_generic o Theory;
   12.20  
   12.21  fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   12.22  

    13.1 --- a/src/Pure/context_position.ML	Sun Mar 18 12:51:44 2012 +0100
    13.2 +++ b/src/Pure/context_position.ML	Sun Mar 18 13:04:22 2012 +0100
    13.3 @@ -12,6 +12,7 @@
    13.4    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
    13.5    val is_visible_proof: Context.generic -> bool
    13.6    val if_visible_proof: Context.generic -> ('a -> unit) -> 'a -> unit
    13.7 +  val report_generic: Context.generic -> Position.T -> Markup.T -> unit
    13.8    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
    13.9    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   13.10    val report: Proof.context -> Position.T -> Markup.T -> unit
   13.11 @@ -33,6 +34,11 @@
   13.12  
   13.13  fun if_visible_proof context f x = if is_visible_proof context then f x else ();
   13.14  
   13.15 +fun report_generic context pos markup =
   13.16 +  if Config.get_generic context visible then
   13.17 +    Output.report (Position.reported_text pos markup "")
   13.18 +  else ();
   13.19 +
   13.20  fun reported_text ctxt pos markup txt =
   13.21    if is_visible ctxt then Position.reported_text pos markup txt else "";
   13.22  

    14.1 --- a/src/Pure/display.ML	Sun Mar 18 12:51:44 2012 +0100
    14.2 +++ b/src/Pure/display.ML	Sun Mar 18 13:04:22 2012 +0100
    14.3 @@ -185,7 +185,8 @@
    14.4      val axioms = (Theory.axiom_space thy, Theory.axiom_table thy);
    14.5      val defs = Theory.defs_of thy;
    14.6      val {restricts, reducts} = Defs.dest defs;
    14.7 -    val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
    14.8 +    val tsig = Sign.tsig_of thy;
    14.9 +    val consts = Sign.consts_of thy;
   14.10      val {constants, constraints} = Consts.dest consts;
   14.11      val extern_const = Name_Space.extern ctxt (#1 constants);
   14.12      val {classes, default, types, ...} = Type.rep_tsig tsig;

    15.1 --- a/src/Pure/facts.ML	Sun Mar 18 12:51:44 2012 +0100
    15.2 +++ b/src/Pure/facts.ML	Sun Mar 18 13:04:22 2012 +0100
    15.3 @@ -32,10 +32,9 @@
    15.4    val props: T -> thm list
    15.5    val could_unify: T -> term -> thm list
    15.6    val merge: T * T -> T
    15.7 -  val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
    15.8 -  val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
    15.9 -  val add_dynamic: Proof.context -> Name_Space.naming ->
   15.10 -    binding * (Context.generic -> thm list) -> T -> string * T
   15.11 +  val add_global: Context.generic -> binding * thm list -> T -> string * T
   15.12 +  val add_local: Context.generic -> bool -> binding * thm list -> T -> string * T
   15.13 +  val add_dynamic: Context.generic -> binding * (Context.generic -> thm list) -> T -> string * T
   15.14    val del: string -> T -> T
   15.15    val hide: bool -> string -> T -> T
   15.16  end;
   15.17 @@ -191,11 +190,11 @@
   15.18  
   15.19  local
   15.20  
   15.21 -fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
   15.22 +fun add context strict do_props (b, ths) (Facts {facts, props}) =
   15.23    let
   15.24      val (name, facts') =
   15.25        if Binding.is_empty b then ("", facts)
   15.26 -      else Name_Space.define ctxt strict naming (b, Static ths) facts;
   15.27 +      else Name_Space.define context strict (b, Static ths) facts;
   15.28      val props' =
   15.29        if do_props
   15.30        then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   15.31 @@ -204,16 +203,16 @@
   15.32  
   15.33  in
   15.34  
   15.35 -fun add_global ctxt = add ctxt true false;
   15.36 -fun add_local ctxt = add ctxt false;
   15.37 +fun add_global context = add context true false;
   15.38 +fun add_local context = add context false;
   15.39  
   15.40  end;
   15.41  
   15.42  
   15.43  (* add dynamic entries *)
   15.44  
   15.45 -fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
   15.46 -  let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
   15.47 +fun add_dynamic context (b, f) (Facts {facts, props}) =
   15.48 +  let val (name, facts') = Name_Space.define context true (b, Dynamic f) facts;
   15.49    in (name, make_facts facts' props) end;
   15.50  
   15.51  

    16.1 --- a/src/Pure/global_theory.ML	Sun Mar 18 12:51:44 2012 +0100
    16.2 +++ b/src/Pure/global_theory.ML	Sun Mar 18 13:04:22 2012 +0100
    16.3 @@ -156,13 +156,11 @@
    16.4    then app_att thms thy |-> register_proofs
    16.5    else
    16.6      let
    16.7 -      val naming = Sign.naming_of thy;
    16.8 -      val name = Name_Space.full_name naming b;
    16.9 +      val name = Sign.full_name thy b;
   16.10        val (thms', thy') = app_att (pre_name name thms) thy |>> post_name name |-> register_proofs;
   16.11        val thms'' = map (Thm.transfer thy') thms';
   16.12        val thy'' = thy'
   16.13 -        |> (Data.map o apfst)
   16.14 -            (Facts.add_global (Proof_Context.init_global thy') naming (b, thms'') #> snd);
   16.15 +        |> (Data.map o apfst) (Facts.add_global (Context.Theory thy') (b, thms'') #> snd);
   16.16      in (thms'', thy'') end;
   16.17  
   16.18  
   16.19 @@ -196,8 +194,7 @@
   16.20  (* add_thms_dynamic *)
   16.21  
   16.22  fun add_thms_dynamic (b, f) thy = thy
   16.23 -  |> (Data.map o apfst)
   16.24 -      (Facts.add_dynamic (Proof_Context.init_global thy) (Sign.naming_of thy) (b, f) #> snd);
   16.25 +  |> (Data.map o apfst) (Facts.add_dynamic (Context.Theory thy) (b, f) #> snd);
   16.26  
   16.27  
   16.28  (* note_thmss *)

    17.1 --- a/src/Pure/sign.ML	Sun Mar 18 12:51:44 2012 +0100
    17.2 +++ b/src/Pure/sign.ML	Sun Mar 18 13:04:22 2012 +0100
    17.3 @@ -7,17 +7,6 @@
    17.4  
    17.5  signature SIGN =
    17.6  sig
    17.7 -  val rep_sg: theory ->
    17.8 -   {naming: Name_Space.naming,
    17.9 -    syn: Syntax.syntax,
   17.10 -    tsig: Type.tsig,
   17.11 -    consts: Consts.T}
   17.12 -  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
   17.13 -  val naming_of: theory -> Name_Space.naming
   17.14 -  val full_name: theory -> binding -> string
   17.15 -  val full_name_path: theory -> string -> binding -> string
   17.16 -  val full_bname: theory -> bstring -> string
   17.17 -  val full_bname_path: theory -> string -> bstring -> string
   17.18    val syn_of: theory -> Syntax.syntax
   17.19    val tsig_of: theory -> Type.tsig
   17.20    val classes_of: theory -> Sorts.algebra
   17.21 @@ -42,6 +31,14 @@
   17.22    val the_const_type: theory -> string -> typ
   17.23    val declared_tyname: theory -> string -> bool
   17.24    val declared_const: theory -> string -> bool
   17.25 +  val naming_of: theory -> Name_Space.naming
   17.26 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
   17.27 +  val restore_naming: theory -> theory -> theory
   17.28 +  val inherit_naming: theory -> Proof.context -> Context.generic
   17.29 +  val full_name: theory -> binding -> string
   17.30 +  val full_name_path: theory -> string -> binding -> string
   17.31 +  val full_bname: theory -> bstring -> string
   17.32 +  val full_bname_path: theory -> string -> bstring -> string
   17.33    val const_monomorphic: theory -> string -> bool
   17.34    val const_typargs: theory -> string * typ -> typ list
   17.35    val const_instance: theory -> string * typ list -> typ
   17.36 @@ -67,7 +64,7 @@
   17.37    val cert_prop: theory -> term -> term
   17.38    val no_frees: Proof.context -> term -> term
   17.39    val no_vars: Proof.context -> term -> term
   17.40 -  val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
   17.41 +  val add_type: Proof.context -> binding * int * mixfix -> theory -> theory
   17.42    val add_types_global: (binding * int * mixfix) list -> theory -> theory
   17.43    val add_nonterminals: Proof.context -> binding list -> theory -> theory
   17.44    val add_nonterminals_global: binding list -> theory -> theory
   17.45 @@ -113,7 +110,6 @@
   17.46    val mandatory_path: string -> theory -> theory
   17.47    val qualified_path: bool -> binding -> theory -> theory
   17.48    val local_path: theory -> theory
   17.49 -  val restore_naming: theory -> theory -> theory
   17.50    val hide_class: bool -> string -> theory -> theory
   17.51    val hide_type: bool -> string -> theory -> theory
   17.52    val hide_const: bool -> string -> theory -> theory
   17.53 @@ -125,56 +121,37 @@
   17.54  (** datatype sign **)
   17.55  
   17.56  datatype sign = Sign of
   17.57 - {naming: Name_Space.naming,    (*common naming conventions*)
   17.58 -  syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   17.59 + {syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
   17.60    tsig: Type.tsig,              (*order-sorted signature of types*)
   17.61    consts: Consts.T};            (*polymorphic constants*)
   17.62  
   17.63 -fun make_sign (naming, syn, tsig, consts) =
   17.64 -  Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
   17.65 +fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
   17.66  
   17.67  structure Data = Theory_Data_PP
   17.68  (
   17.69    type T = sign;
   17.70 -  fun extend (Sign {syn, tsig, consts, ...}) =
   17.71 -    make_sign (Name_Space.default_naming, syn, tsig, consts);
   17.72 +  fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
   17.73  
   17.74 -  val empty =
   17.75 -    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   17.76 +  val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   17.77  
   17.78    fun merge pp (sign1, sign2) =
   17.79      let
   17.80 -      val ctxt = Syntax.init_pretty pp;
   17.81 -      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   17.82 -      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   17.83 +      val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   17.84 +      val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   17.85  
   17.86 -      val naming = Name_Space.default_naming;
   17.87        val syn = Syntax.merge_syntax (syn1, syn2);
   17.88 -      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
   17.89 +      val tsig = Type.merge_tsig pp (tsig1, tsig2);
   17.90        val consts = Consts.merge (consts1, consts2);
   17.91 -    in make_sign (naming, syn, tsig, consts) end;
   17.92 +    in make_sign (syn, tsig, consts) end;
   17.93  );
   17.94  
   17.95  fun rep_sg thy = Data.get thy |> (fn Sign args => args);
   17.96  
   17.97 -fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
   17.98 -  make_sign (f (naming, syn, tsig, consts)));
   17.99 +fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
  17.100  
  17.101 -fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
  17.102 -fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
  17.103 -fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
  17.104 -fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
  17.105 -
  17.106 -
  17.107 -(* naming *)
  17.108 -
  17.109 -val naming_of = #naming o rep_sg;
  17.110 -
  17.111 -val full_name = Name_Space.full_name o naming_of;
  17.112 -fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
  17.113 -
  17.114 -fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
  17.115 -fun full_bname_path thy path = full_name_path thy path o Binding.name;
  17.116 +fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
  17.117 +fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
  17.118 +fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
  17.119  
  17.120  
  17.121  (* syntax *)
  17.122 @@ -222,6 +199,21 @@
  17.123  val declared_const = can o the_const_constraint;
  17.124  
  17.125  
  17.126 +(* naming *)
  17.127 +
  17.128 +val naming_of = Name_Space.naming_of o Context.Theory;
  17.129 +val map_naming = Context.theory_map o Name_Space.map_naming;
  17.130 +val restore_naming = map_naming o K o naming_of;
  17.131 +fun inherit_naming thy =
  17.132 +  Context.Proof o Context.proof_map (Name_Space.map_naming (K (naming_of thy)));
  17.133 +
  17.134 +val full_name = Name_Space.full_name o naming_of;
  17.135 +fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
  17.136 +
  17.137 +fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
  17.138 +fun full_bname_path thy path = full_name_path thy path o Binding.name;
  17.139 +
  17.140 +
  17.141  
  17.142  (** name spaces **)
  17.143  
  17.144 @@ -330,22 +322,21 @@
  17.145  
  17.146  (* add type constructors *)
  17.147  
  17.148 -fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
  17.149 +fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
  17.150    let
  17.151 -    fun type_syntax (b, n, mx) =
  17.152 -      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
  17.153 -    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
  17.154 -    val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
  17.155 -  in (naming, syn', tsig', consts) end);
  17.156 +    val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
  17.157 +    val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
  17.158 +    val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
  17.159 +  in (syn', tsig', consts) end);
  17.160  
  17.161  fun add_types_global types thy =
  17.162 -  add_types (Syntax.init_pretty_global thy) types thy;
  17.163 +  fold (add_type (Syntax.init_pretty_global thy)) types thy;
  17.164  
  17.165  
  17.166  (* add nonterminals *)
  17.167  
  17.168 -fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
  17.169 -  (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
  17.170 +fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) =>
  17.171 +  (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts));
  17.172  
  17.173  fun add_nonterminals_global ns thy =
  17.174    add_nonterminals (Syntax.init_pretty_global thy) ns thy;
  17.175 @@ -353,8 +344,8 @@
  17.176  
  17.177  (* add type abbreviations *)
  17.178  
  17.179 -fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
  17.180 -  (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
  17.181 +fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) =>
  17.182 +  (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts));
  17.183  
  17.184  
  17.185  (* modify syntax *)
  17.186 @@ -409,7 +400,7 @@
  17.187      val args = map prep raw_args;
  17.188    in
  17.189      thy
  17.190 -    |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
  17.191 +    |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
  17.192      |> add_syntax_i (map #2 args)
  17.193      |> pair (map #3 args)
  17.194    end;
  17.195 @@ -437,7 +428,7 @@
  17.196      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
  17.197        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
  17.198      val (res, consts') = consts_of thy
  17.199 -      |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
  17.200 +      |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t);
  17.201    in (res, thy |> map_consts (K consts')) end;
  17.202  
  17.203  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
  17.204 @@ -458,18 +449,16 @@
  17.205  
  17.206  fun primitive_class (bclass, classes) thy =
  17.207    thy
  17.208 -  |> map_sign (fn (naming, syn, tsig, consts) =>
  17.209 -    let
  17.210 -      val ctxt = Syntax.init_pretty_global thy;
  17.211 -      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
  17.212 -    in (naming, syn, tsig', consts) end)
  17.213 +  |> map_sign (fn (syn, tsig, consts) =>
  17.214 +      let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
  17.215 +      in (syn, tsig', consts) end)
  17.216    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  17.217  
  17.218  fun primitive_classrel arg thy =
  17.219 -  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
  17.220 +  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
  17.221  
  17.222  fun primitive_arity arg thy =
  17.223 -  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
  17.224 +  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
  17.225  
  17.226  
  17.227  (* add translation functions *)
  17.228 @@ -512,8 +501,6 @@
  17.229  
  17.230  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
  17.231  
  17.232 -val restore_naming = map_naming o K o naming_of;
  17.233 -
  17.234  
  17.235  (* hide names *)
  17.236  

    18.1 --- a/src/Pure/simplifier.ML	Sun Mar 18 12:51:44 2012 +0100
    18.2 +++ b/src/Pure/simplifier.ML	Sun Mar 18 13:04:22 2012 +0100
    18.3 @@ -171,7 +171,7 @@
    18.4  
    18.5  (* get simprocs *)
    18.6  
    18.7 -fun check_simproc ctxt = Name_Space.check ctxt (get_simprocs ctxt) #> #1;
    18.8 +fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
    18.9  val the_simproc = Name_Space.get o get_simprocs;
   18.10  
   18.11  val _ =
   18.12 @@ -202,14 +202,12 @@
   18.13    in
   18.14      lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context =>
   18.15        let
   18.16 -        val naming = Proof_Context.target_naming_of context;
   18.17          val b' = Morphism.binding phi b;
   18.18          val simproc' = transform_simproc phi simproc;
   18.19        in
   18.20          context
   18.21          |> Data.map (fn (ss, tab) =>
   18.22 -          (ss addsimprocs [simproc'],
   18.23 -            #2 (Name_Space.define (Context.proof_of context) true naming (b', simproc') tab)))
   18.24 +          (ss addsimprocs [simproc'], #2 (Name_Space.define context true (b', simproc') tab)))
   18.25        end)
   18.26    end;
   18.27  

    19.1 --- a/src/Pure/sorts.ML	Sun Mar 18 12:51:44 2012 +0100
    19.2 +++ b/src/Pure/sorts.ML	Sun Mar 18 13:04:22 2012 +0100
    19.3 @@ -38,15 +38,15 @@
    19.4    val minimize_sort: algebra -> sort -> sort
    19.5    val complete_sort: algebra -> sort -> sort
    19.6    val minimal_sorts: algebra -> sort list -> sort Ord_List.T
    19.7 -  val add_class: Proof.context -> class * class list -> algebra -> algebra
    19.8 -  val add_classrel: Proof.context -> class * class -> algebra -> algebra
    19.9 -  val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
   19.10 +  val add_class: Context.pretty -> class * class list -> algebra -> algebra
   19.11 +  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
   19.12 +  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
   19.13    val empty_algebra: algebra
   19.14 -  val merge_algebra: Proof.context -> algebra * algebra -> algebra
   19.15 -  val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
   19.16 +  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
   19.17 +  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
   19.18      -> algebra -> (sort -> sort) * algebra
   19.19    type class_error
   19.20 -  val class_error: Proof.context -> class_error -> string
   19.21 +  val class_error: Context.pretty -> class_error -> string
   19.22    exception CLASS_ERROR of class_error
   19.23    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   19.24    val meet_sort: algebra -> typ * sort
   19.25 @@ -187,16 +187,16 @@
   19.26  
   19.27  fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
   19.28  
   19.29 -fun err_cyclic_classes ctxt css =
   19.30 +fun err_cyclic_classes pp css =
   19.31    error (cat_lines (map (fn cs =>
   19.32 -    "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
   19.33 +    "Cycle in class relation: " ^ Syntax.string_of_classrel (Syntax.init_pretty pp) cs) css));
   19.34  
   19.35 -fun add_class ctxt (c, cs) = map_classes (fn classes =>
   19.36 +fun add_class pp (c, cs) = map_classes (fn classes =>
   19.37    let
   19.38      val classes' = classes |> Graph.new_node (c, serial ())
   19.39        handle Graph.DUP dup => err_dup_class dup;
   19.40      val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
   19.41 -      handle Graph.CYCLES css => err_cyclic_classes ctxt css;
   19.42 +      handle Graph.CYCLES css => err_cyclic_classes pp css;
   19.43    in classes'' end);
   19.44  
   19.45  
   19.46 @@ -207,12 +207,14 @@
   19.47  fun for_classes _ NONE = ""
   19.48    | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
   19.49  
   19.50 -fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
   19.51 -  error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
   19.52 -    Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
   19.53 -    Syntax.string_of_arity ctxt (t, Ss', [c']));
   19.54 +fun err_conflict pp t cc (c, Ss) (c', Ss') =
   19.55 +  let val ctxt = Syntax.init_pretty pp in
   19.56 +    error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
   19.57 +      Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
   19.58 +      Syntax.string_of_arity ctxt (t, Ss', [c']))
   19.59 +  end;
   19.60  
   19.61 -fun coregular ctxt algebra t (c, Ss) ars =
   19.62 +fun coregular pp algebra t (c, Ss) ars =
   19.63    let
   19.64      fun conflict (c', Ss') =
   19.65        if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
   19.66 @@ -222,62 +224,62 @@
   19.67        else NONE;
   19.68    in
   19.69      (case get_first conflict ars of
   19.70 -      SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
   19.71 +      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
   19.72      | NONE => (c, Ss) :: ars)
   19.73    end;
   19.74  
   19.75  fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
   19.76  
   19.77 -fun insert ctxt algebra t (c, Ss) ars =
   19.78 +fun insert pp algebra t (c, Ss) ars =
   19.79    (case AList.lookup (op =) ars c of
   19.80 -    NONE => coregular ctxt algebra t (c, Ss) ars
   19.81 +    NONE => coregular pp algebra t (c, Ss) ars
   19.82    | SOME Ss' =>
   19.83        if sorts_le algebra (Ss, Ss') then ars
   19.84        else if sorts_le algebra (Ss', Ss)
   19.85 -      then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
   19.86 -      else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
   19.87 +      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
   19.88 +      else err_conflict pp t NONE (c, Ss) (c, Ss'));
   19.89  
   19.90  in
   19.91  
   19.92 -fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
   19.93 +fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
   19.94  
   19.95 -fun insert_complete_ars ctxt algebra (t, ars) arities =
   19.96 +fun insert_complete_ars pp algebra (t, ars) arities =
   19.97    let val ars' =
   19.98      Symtab.lookup_list arities t
   19.99 -    |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
  19.100 +    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
  19.101    in Symtab.update (t, ars') arities end;
  19.102  
  19.103 -fun add_arities ctxt arg algebra =
  19.104 -  algebra |> map_arities (insert_complete_ars ctxt algebra arg);
  19.105 +fun add_arities pp arg algebra =
  19.106 +  algebra |> map_arities (insert_complete_ars pp algebra arg);
  19.107  
  19.108 -fun add_arities_table ctxt algebra =
  19.109 -  Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
  19.110 +fun add_arities_table pp algebra =
  19.111 +  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
  19.112  
  19.113  end;
  19.114  
  19.115  
  19.116  (* classrel *)
  19.117  
  19.118 -fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
  19.119 +fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
  19.120    Symtab.empty
  19.121 -  |> add_arities_table ctxt algebra arities);
  19.122 +  |> add_arities_table pp algebra arities);
  19.123  
  19.124 -fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
  19.125 +fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
  19.126    classes |> Graph.add_edge_trans_acyclic rel
  19.127 -    handle Graph.CYCLES css => err_cyclic_classes ctxt css);
  19.128 +    handle Graph.CYCLES css => err_cyclic_classes pp css);
  19.129  
  19.130  
  19.131  (* empty and merge *)
  19.132  
  19.133  val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
  19.134  
  19.135 -fun merge_algebra ctxt
  19.136 +fun merge_algebra pp
  19.137     (Algebra {classes = classes1, arities = arities1},
  19.138      Algebra {classes = classes2, arities = arities2}) =
  19.139    let
  19.140      val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
  19.141        handle Graph.DUP c => err_dup_class c
  19.142 -        | Graph.CYCLES css => err_cyclic_classes ctxt css;
  19.143 +        | Graph.CYCLES css => err_cyclic_classes pp css;
  19.144      val algebra0 = make_algebra (classes', Symtab.empty);
  19.145      val arities' =
  19.146        (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
  19.147 @@ -285,20 +287,20 @@
  19.148        | (true, false) =>  (*no completion*)
  19.149            (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
  19.150              if pointer_eq (ars1, ars2) then raise Symtab.SAME
  19.151 -            else insert_ars ctxt algebra0 t ars2 ars1)
  19.152 +            else insert_ars pp algebra0 t ars2 ars1)
  19.153        | (false, true) =>  (*unary completion*)
  19.154            Symtab.empty
  19.155 -          |> add_arities_table ctxt algebra0 arities1
  19.156 +          |> add_arities_table pp algebra0 arities1
  19.157        | (false, false) => (*binary completion*)
  19.158            Symtab.empty
  19.159 -          |> add_arities_table ctxt algebra0 arities1
  19.160 -          |> add_arities_table ctxt algebra0 arities2);
  19.161 +          |> add_arities_table pp algebra0 arities1
  19.162 +          |> add_arities_table pp algebra0 arities2);
  19.163    in make_algebra (classes', arities') end;
  19.164  
  19.165  
  19.166  (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
  19.167  
  19.168 -fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
  19.169 +fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
  19.170    let
  19.171      val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
  19.172      fun restrict_arity t (c, Ss) =
  19.173 @@ -310,7 +312,7 @@
  19.174        else NONE;
  19.175      val classes' = classes |> Graph.restrict P;
  19.176      val arities' = arities |> Symtab.map (map_filter o restrict_arity);
  19.177 -  in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
  19.178 +  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
  19.179  
  19.180  
  19.181  
  19.182 @@ -323,13 +325,14 @@
  19.183    No_Arity of string * class |
  19.184    No_Subsort of sort * sort;
  19.185  
  19.186 -fun class_error ctxt (No_Classrel (c1, c2)) =
  19.187 -      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
  19.188 -  | class_error ctxt (No_Arity (a, c)) =
  19.189 -      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
  19.190 -  | class_error ctxt (No_Subsort (S1, S2)) =
  19.191 -      "Cannot derive subsort relation " ^
  19.192 -        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
  19.193 +fun class_error pp =
  19.194 +  let val ctxt = Syntax.init_pretty pp in
  19.195 +    fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
  19.196 +     | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
  19.197 +     | No_Subsort (S1, S2) =>
  19.198 +        "Cannot derive subsort relation " ^
  19.199 +          Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2
  19.200 +  end;
  19.201  
  19.202  exception CLASS_ERROR of class_error;
  19.203  

    20.1 --- a/src/Pure/theory.ML	Sun Mar 18 12:51:44 2012 +0100
    20.2 +++ b/src/Pure/theory.ML	Sun Mar 18 13:04:22 2012 +0100
    20.3 @@ -177,7 +177,7 @@
    20.4  fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
    20.5    let
    20.6      val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
    20.7 -    val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
    20.8 +    val (_, axioms') = Name_Space.define (Sign.inherit_naming thy ctxt) true axm axioms;
    20.9    in axioms' end);
   20.10  
   20.11  

    21.1 --- a/src/Pure/thm.ML	Sun Mar 18 12:51:44 2012 +0100
    21.2 +++ b/src/Pure/thm.ML	Sun Mar 18 13:04:22 2012 +0100
    21.3 @@ -1772,9 +1772,7 @@
    21.4  
    21.5  fun add_oracle (b, oracle) thy =
    21.6    let
    21.7 -    val naming = Sign.naming_of thy;
    21.8 -    val (name, tab') =
    21.9 -      Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
   21.10 +    val (name, tab') = Name_Space.define (Context.Theory thy) true (b, ()) (Oracles.get thy);
   21.11      val thy' = Oracles.put tab' thy;
   21.12    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
   21.13  

    22.1 --- a/src/Pure/type.ML	Sun Mar 18 12:51:44 2012 +0100
    22.2 +++ b/src/Pure/type.ML	Sun Mar 18 13:04:22 2012 +0100
    22.3 @@ -87,16 +87,16 @@
    22.4    val eq_type: tyenv -> typ * typ -> bool
    22.5  
    22.6    (*extend and merge type signatures*)
    22.7 -  val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
    22.8 +  val add_class: Context.generic -> binding * class list -> tsig -> tsig
    22.9    val hide_class: bool -> string -> tsig -> tsig
   22.10    val set_defsort: sort -> tsig -> tsig
   22.11 -  val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
   22.12 -  val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   22.13 -  val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   22.14 +  val add_type: Context.generic -> binding * int -> tsig -> tsig
   22.15 +  val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
   22.16 +  val add_nonterminal: Context.generic -> binding -> tsig -> tsig
   22.17    val hide_type: bool -> string -> tsig -> tsig
   22.18 -  val add_arity: Proof.context -> arity -> tsig -> tsig
   22.19 -  val add_classrel: Proof.context -> class * class -> tsig -> tsig
   22.20 -  val merge_tsig: Proof.context -> tsig * tsig -> tsig
   22.21 +  val add_arity: Context.pretty -> arity -> tsig -> tsig
   22.22 +  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
   22.23 +  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
   22.24  end;
   22.25  
   22.26  structure Type: TYPE =
   22.27 @@ -318,8 +318,9 @@
   22.28    | _ => error (undecl_type a));
   22.29  
   22.30  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   22.31 -  | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
   22.32 -      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
   22.33 +  | arity_sorts pp (TSig {classes, ...}) a S =
   22.34 +      Sorts.mg_domain (#2 classes) a S
   22.35 +        handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
   22.36  
   22.37  
   22.38  
   22.39 @@ -584,14 +585,14 @@
   22.40  
   22.41  (* classes *)
   22.42  
   22.43 -fun add_class ctxt naming (c, cs) tsig =
   22.44 +fun add_class context (c, cs) tsig =
   22.45    tsig |> map_tsig (fn ((space, classes), default, types) =>
   22.46      let
   22.47        val cs' = map (cert_class tsig) cs
   22.48          handle TYPE (msg, _, _) => error msg;
   22.49        val _ = Binding.check c;
   22.50 -      val (c', space') = space |> Name_Space.declare ctxt true naming c;
   22.51 -      val classes' = classes |> Sorts.add_class ctxt (c', cs');
   22.52 +      val (c', space') = space |> Name_Space.declare context true c;
   22.53 +      val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
   22.54      in ((space', classes'), default, types) end);
   22.55  
   22.56  fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
   22.57 @@ -600,7 +601,7 @@
   22.58  
   22.59  (* arities *)
   22.60  
   22.61 -fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   22.62 +fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   22.63    let
   22.64      val _ =
   22.65        (case lookup_type tsig t of
   22.66 @@ -609,18 +610,18 @@
   22.67        | NONE => error (undecl_type t));
   22.68      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   22.69        handle TYPE (msg, _, _) => error msg;
   22.70 -    val classes' = classes |> Sorts.add_arities ctxt ((t, map (fn c' => (c', Ss')) S'));
   22.71 +    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   22.72    in ((space, classes'), default, types) end);
   22.73  
   22.74  
   22.75  (* classrel *)
   22.76  
   22.77 -fun add_classrel ctxt rel tsig =
   22.78 +fun add_classrel pp rel tsig =
   22.79    tsig |> map_tsig (fn ((space, classes), default, types) =>
   22.80      let
   22.81        val rel' = pairself (cert_class tsig) rel
   22.82          handle TYPE (msg, _, _) => error msg;
   22.83 -      val classes' = classes |> Sorts.add_classrel ctxt rel';
   22.84 +      val classes' = classes |> Sorts.add_classrel pp rel';
   22.85      in ((space, classes'), default, types) end);
   22.86  
   22.87  
   22.88 @@ -634,8 +635,8 @@
   22.89  
   22.90  local
   22.91  
   22.92 -fun new_decl ctxt naming (c, decl) types =
   22.93 -  (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
   22.94 +fun new_decl context (c, decl) types =
   22.95 +  (Binding.check c; #2 (Name_Space.define context true (c, decl) types));
   22.96  
   22.97  fun map_types f = map_tsig (fn (classes, default, types) =>
   22.98    let
   22.99 @@ -651,11 +652,11 @@
  22.100  
  22.101  in
  22.102  
  22.103 -fun add_type ctxt naming (c, n) =
  22.104 +fun add_type context (c, n) =
  22.105    if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
  22.106 -  else map_types (new_decl ctxt naming (c, LogicalType n));
  22.107 +  else map_types (new_decl context (c, LogicalType n));
  22.108  
  22.109 -fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
  22.110 +fun add_abbrev context (a, vs, rhs) tsig = tsig |> map_types (fn types =>
  22.111    let
  22.112      fun err msg =
  22.113        cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
  22.114 @@ -669,9 +670,9 @@
  22.115        (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
  22.116          [] => []
  22.117        | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
  22.118 -  in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
  22.119 +  in types |> new_decl context (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
  22.120  
  22.121 -fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
  22.122 +fun add_nonterminal context = map_types o new_decl context o rpair Nonterminal;
  22.123  
  22.124  end;
  22.125  
  22.126 @@ -681,7 +682,7 @@
  22.127  
  22.128  (* merge type signatures *)
  22.129  
  22.130 -fun merge_tsig ctxt (tsig1, tsig2) =
  22.131 +fun merge_tsig pp (tsig1, tsig2) =
  22.132    let
  22.133      val (TSig {classes = (space1, classes1), default = default1, types = types1,
  22.134        log_types = _}) = tsig1;
  22.135 @@ -689,7 +690,7 @@
  22.136        log_types = _}) = tsig2;
  22.137  
  22.138      val space' = Name_Space.merge (space1, space2);
  22.139 -    val classes' = Sorts.merge_algebra ctxt (classes1, classes2);
  22.140 +    val classes' = Sorts.merge_algebra pp (classes1, classes2);
  22.141      val default' = Sorts.inter_sort classes' (default1, default2);
  22.142      val types' = Name_Space.merge_tables (types1, types2);
  22.143    in build_tsig ((space', classes'), default', types') end;

    23.1 --- a/src/Pure/variable.ML	Sun Mar 18 12:51:44 2012 +0100
    23.2 +++ b/src/Pure/variable.ML	Sun Mar 18 13:04:22 2012 +0100
    23.3 @@ -341,12 +341,14 @@
    23.4  fun new_fixed ((x, x'), pos) ctxt =
    23.5    if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
    23.6    else
    23.7 -    ctxt
    23.8 -    |> map_fixes
    23.9 -      (Name_Space.define ctxt true Name_Space.default_naming (Binding.make (x', pos), x) #> snd #>>
   23.10 -        Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
   23.11 -    |> declare_fixed x
   23.12 -    |> declare_constraints (Syntax.free x');
   23.13 +    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
   23.14 +      ctxt
   23.15 +      |> map_fixes
   23.16 +        (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>>
   23.17 +          Name_Space.alias Name_Space.default_naming (Binding.make (x, pos)) x')
   23.18 +      |> declare_fixed x
   23.19 +      |> declare_constraints (Syntax.free x')
   23.20 +  end;
   23.21  
   23.22  fun new_fixes names' xs xs' ps =
   23.23    map_names (K names') #>

    24.1 --- a/src/Tools/Code/code_preproc.ML	Sun Mar 18 12:51:44 2012 +0100
    24.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Mar 18 13:04:22 2012 +0100
    24.3 @@ -431,7 +431,7 @@
    24.4        |> fold (ensure_fun thy arities eqngr) cs
    24.5        |> fold (ensure_rhs thy arities eqngr) cs_rhss;
    24.6      val arities' = fold (add_arity thy vardeps) insts arities;
    24.7 -    val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
    24.8 +    val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
    24.9        (AList.lookup (op =) arities') (Sign.classes_of thy);
   24.10      val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
   24.11      fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)

    25.1 --- a/src/Tools/Code/code_thingol.ML	Sun Mar 18 12:51:44 2012 +0100
    25.2 +++ b/src/Tools/Code/code_thingol.ML	Sun Mar 18 13:04:22 2012 +0100
    25.3 @@ -571,10 +571,9 @@
    25.4  
    25.5  fun not_wellsorted thy permissive some_thm ty sort e =
    25.6    let
    25.7 -    val ctxt = Syntax.init_pretty_global thy;
    25.8 -    val err_class = Sorts.class_error ctxt e;
    25.9 +    val err_class = Sorts.class_error (Context.pretty_global thy) e;
   25.10      val err_typ =
   25.11 -      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
   25.12 +      "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " ^
   25.13          Syntax.string_of_sort_global thy sort;
   25.14    in
   25.15      translation_error thy permissive some_thm "Wellsortedness error"
   25.16 @@ -1001,7 +1000,7 @@
   25.17  fun read_const_exprs thy =
   25.18    let
   25.19      fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
   25.20 -      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
   25.21 +      ((snd o #constants o Consts.dest o Sign.consts_of) thy') [];
   25.22      fun belongs_here thy' c = forall
   25.23        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
   25.24      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');