prefer local name spaces;
authorwenzelm
Sat Apr 16 15:25:25 2011 +0200 (2011-04-16)
changeset 423596ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
prefer local name spaces;
tuned signatures;
tuned;
src/HOL/List.thy
src/HOL/Tools/Datatype/datatype_case.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/record.ML
src/Pure/Isar/class.ML
src/Pure/Isar/code.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Pure/display.ML
src/Pure/sign.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/List.thy	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/HOL/List.thy	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -396,7 +396,7 @@
     1.4    fun abs_tr ctxt (p as Free (s, T)) e opti =
     1.5          let
     1.6            val thy = ProofContext.theory_of ctxt;
     1.7 -          val s' = Sign.intern_const thy s;
     1.8 +          val s' = ProofContext.intern_const ctxt s;
     1.9          in
    1.10            if Sign.declared_const thy s'
    1.11            then (pat_tr ctxt p e opti, false)
     2.1 --- a/src/HOL/Tools/Datatype/datatype_case.ML	Sat Apr 16 13:48:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_case.ML	Sat Apr 16 15:25:25 2011 +0200
     2.3 @@ -307,7 +307,7 @@
     2.4  fun case_tr err tab_of ctxt [t, u] =
     2.5        let
     2.6          val thy = ProofContext.theory_of ctxt;
     2.7 -        val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy);
     2.8 +        val intern_const_syntax = Consts.intern_syntax (ProofContext.consts_of ctxt);
     2.9  
    2.10          (* replace occurrences of dummy_pattern by distinct variables *)
    2.11          (* internalize constant names                                 *)
    2.12 @@ -320,7 +320,7 @@
    2.13            | prep_pat (Const (s, T)) used =
    2.14                (Const (intern_const_syntax s, T), used)
    2.15            | prep_pat (v as Free (s, T)) used =
    2.16 -              let val s' = Sign.intern_const thy s in
    2.17 +              let val s' = ProofContext.intern_const ctxt s in
    2.18                  if Sign.declared_const thy s' then
    2.19                    (Const (s', T), used)
    2.20                  else (v, used)
    2.21 @@ -328,7 +328,7 @@
    2.22            | prep_pat (t $ u) used =
    2.23                let
    2.24                  val (t', used') = prep_pat t used;
    2.25 -                val (u', used'') = prep_pat u used'
    2.26 +                val (u', used'') = prep_pat u used';
    2.27                in
    2.28                  (t' $ u', used'')
    2.29                end
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Sat Apr 16 13:48:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Sat Apr 16 15:25:25 2011 +0200
     3.3 @@ -378,12 +378,13 @@
     3.4  
     3.5  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
     3.6    let
     3.7 +    val ctxt = ProofContext.init_global thy;
     3.8 +
     3.9      fun constr_of_term (Const (c, T)) = (c, T)
    3.10 -      | constr_of_term t =
    3.11 -          error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    3.12 -    fun no_constr (c, T) = error ("Bad constructor: "
    3.13 -      ^ Sign.extern_const thy c ^ "::"
    3.14 -      ^ Syntax.string_of_typ_global thy T);
    3.15 +      | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t);
    3.16 +    fun no_constr (c, T) =
    3.17 +      error ("Bad constructor: " ^ ProofContext.extern_const ctxt c ^ "::" ^
    3.18 +        Syntax.string_of_typ ctxt T);
    3.19      fun type_of_constr (cT as (_, T)) =
    3.20        let
    3.21          val frees = OldTerm.typ_tfrees T;
    3.22 @@ -437,8 +438,7 @@
    3.23          #-> after_qed
    3.24        end;
    3.25    in
    3.26 -    thy
    3.27 -    |> ProofContext.init_global
    3.28 +    ctxt
    3.29      |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules))
    3.30    end;
    3.31  
     4.1 --- a/src/HOL/Tools/record.ML	Sat Apr 16 13:48:45 2011 +0200
     4.2 +++ b/src/HOL/Tools/record.ML	Sat Apr 16 15:25:25 2011 +0200
     4.3 @@ -693,7 +693,7 @@
     4.4        | split_args _ _ = ([], []);
     4.5  
     4.6      fun mk_ext (fargs as (name, _) :: _) =
     4.7 -          (case get_fieldext thy (Sign.intern_const thy name) of
     4.8 +          (case get_fieldext thy (ProofContext.intern_const ctxt name) of
     4.9              SOME (ext, alphas) =>
    4.10                (case get_extfields thy ext of
    4.11                  SOME fields =>
    4.12 @@ -753,7 +753,7 @@
    4.13        | split_args _ _ = ([], []);
    4.14  
    4.15      fun mk_ext (fargs as (name, _) :: _) =
    4.16 -          (case get_fieldext thy (Sign.intern_const thy name) of
    4.17 +          (case get_fieldext thy (ProofContext.intern_const ctxt name) of
    4.18              SOME (ext, _) =>
    4.19                (case get_extfields thy ext of
    4.20                  SOME fields =>
    4.21 @@ -831,7 +831,8 @@
    4.22                       (let
    4.23                          val (f :: fs, _) = split_last fields;
    4.24                          val fields' =
    4.25 -                          apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs;
    4.26 +                          apfst (ProofContext.extern_const ctxt) f ::
    4.27 +                            map (apfst Long_Name.base_name) fs;
    4.28                          val (args', more) = split_last args;
    4.29                          val alphavars = map varifyT (#1 (split_last alphas));
    4.30                          val subst = Type.raw_matches (alphavars, args') Vartab.empty;
    4.31 @@ -914,7 +915,6 @@
    4.32  fun record_tr' ctxt t =
    4.33    let
    4.34      val thy = ProofContext.theory_of ctxt;
    4.35 -    val extern = Consts.extern ctxt (ProofContext.consts_of ctxt);
    4.36  
    4.37      fun strip_fields t =
    4.38        (case strip_comb t of
    4.39 @@ -925,7 +925,7 @@
    4.40                  SOME fields =>
    4.41                   (let
    4.42                      val (f :: fs, _) = split_last (map fst fields);
    4.43 -                    val fields' = extern f :: map Long_Name.base_name fs;
    4.44 +                    val fields' = ProofContext.extern_const ctxt f :: map Long_Name.base_name fs;
    4.45                      val (args', more) = split_last args;
    4.46                    in (fields' ~~ args') @ strip_fields more end
    4.47                    handle ListPair.UnequalLengths => [("", t)])
    4.48 @@ -957,7 +957,7 @@
    4.49  
    4.50  fun dest_update ctxt c =
    4.51    (case try Lexicon.unmark_const c of
    4.52 -    SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d)
    4.53 +    SOME d => try (unsuffix updateN) (ProofContext.extern_const ctxt d)
    4.54    | NONE => NONE);
    4.55  
    4.56  fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
     5.1 --- a/src/Pure/Isar/class.ML	Sat Apr 16 13:48:45 2011 +0200
     5.2 +++ b/src/Pure/Isar/class.ML	Sat Apr 16 15:25:25 2011 +0200
     5.3 @@ -14,7 +14,7 @@
     5.4    val these_defs: theory -> sort -> thm list
     5.5    val these_operations: theory -> sort
     5.6      -> (string * (class * (typ * term))) list
     5.7 -  val print_classes: theory -> unit
     5.8 +  val print_classes: Proof.context -> unit
     5.9    val init: class -> theory -> Proof.context
    5.10    val begin: class list -> sort -> Proof.context -> Proof.context
    5.11    val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
    5.12 @@ -69,7 +69,7 @@
    5.13    assm_intro: thm option,
    5.14    of_class: thm,
    5.15    axiom: thm option,
    5.16 -  
    5.17 +
    5.18    (* dynamic part *)
    5.19    defs: thm list,
    5.20    operations: (string * (class * (typ * term))) list
    5.21 @@ -149,9 +149,9 @@
    5.22    | NONE => base_morphism thy class;
    5.23  val export_morphism = #export_morph oo the_class_data;
    5.24  
    5.25 -fun print_classes thy =
    5.26 +fun print_classes ctxt =
    5.27    let
    5.28 -    val ctxt = ProofContext.init_global thy;
    5.29 +    val thy = ProofContext.theory_of ctxt;
    5.30      val algebra = Sign.classes_of thy;
    5.31      val arities =
    5.32        Symtab.empty
    5.33 @@ -163,10 +163,11 @@
    5.34        let
    5.35          val Ss = Sorts.mg_domain algebra tyco [class];
    5.36        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    5.37 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
    5.38 -      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
    5.39 +    fun mk_param (c, ty) =
    5.40 +      Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^
    5.41 +        Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
    5.42      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    5.43 -      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
    5.44 +      (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"),
    5.45        (SOME o Pretty.block) [Pretty.str "supersort: ",
    5.46          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    5.47        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
    5.48 @@ -500,18 +501,20 @@
    5.49      val thy = ProofContext.theory_of lthy;
    5.50      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    5.51      fun pr_param ((c, _), (v, ty)) =
    5.52 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    5.53 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
    5.54 +      Pretty.block (Pretty.breaks
    5.55 +        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
    5.56 +          Pretty.str "::", Syntax.pretty_typ lthy ty]);
    5.57    in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
    5.58  
    5.59  fun conclude lthy =
    5.60    let
    5.61 -    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    5.62 +    val (tycos, vs, sort) = #arities (the_instantiation lthy);
    5.63      val thy = ProofContext.theory_of lthy;
    5.64 -    val _ = map (fn tyco => if Sign.of_sort thy
    5.65 +    val _ = tycos |> List.app (fn tyco =>
    5.66 +      if Sign.of_sort thy
    5.67          (Type (tyco, map TFree vs), sort)
    5.68 -      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
    5.69 -        tycos;
    5.70 +      then ()
    5.71 +      else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco)));
    5.72    in lthy end;
    5.73  
    5.74  fun instantiation (tycos, vs, sort) thy =
     6.1 --- a/src/Pure/Isar/code.ML	Sat Apr 16 13:48:45 2011 +0200
     6.2 +++ b/src/Pure/Isar/code.ML	Sat Apr 16 15:25:25 2011 +0200
     6.3 @@ -112,9 +112,14 @@
     6.4  fun string_of_typ thy =
     6.5    Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
     6.6  
     6.7 -fun string_of_const thy c = case AxClass.inst_of_param thy c
     6.8 - of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
     6.9 -  | NONE => Sign.extern_const thy c;
    6.10 +fun string_of_const thy c =
    6.11 +  let val ctxt = ProofContext.init_global thy in
    6.12 +    case AxClass.inst_of_param thy c of
    6.13 +      SOME (c, tyco) =>
    6.14 +        ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]"
    6.15 +          (ProofContext.extern_type ctxt tyco)
    6.16 +    | NONE => ProofContext.extern_const ctxt c
    6.17 +  end;
    6.18  
    6.19  
    6.20  (* constants *)
     7.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 13:48:45 2011 +0200
     7.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 15:25:25 2011 +0200
     7.3 @@ -616,7 +616,7 @@
     7.4  fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
     7.5    if length args = n then
     7.6      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
     7.7 -      Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args)
     7.8 +      Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args)
     7.9    else raise Match);
    7.10  
    7.11  (* define one predicate including its intro rule and axioms
     8.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 13:48:45 2011 +0200
     8.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 15:25:25 2011 +0200
     8.3 @@ -162,7 +162,7 @@
     8.4      val ctxt = ProofContext.init_global thy;
     8.5    in
     8.6      raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
     8.7 -      Syntax_Phases.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
     8.8 +      Syntax_Phases.parse_ast_pattern ctxt (ProofContext.intern_type ctxt r, s)))
     8.9    end;
    8.10  
    8.11  fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
     9.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Apr 16 13:48:45 2011 +0200
     9.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 16 15:25:25 2011 +0200
     9.3 @@ -829,8 +829,8 @@
     9.4  
     9.5  val _ =
     9.6    Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
     9.7 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
     9.8 -      o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
     9.9 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
    9.10 +      Toplevel.keep (Class.print_classes o Toplevel.context_of)));
    9.11  
    9.12  val _ =
    9.13    Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
    10.1 --- a/src/Pure/Isar/overloading.ML	Sat Apr 16 13:48:45 2011 +0200
    10.2 +++ b/src/Pure/Isar/overloading.ML	Sat Apr 16 15:25:25 2011 +0200
    10.3 @@ -158,11 +158,11 @@
    10.4  
    10.5  fun pretty lthy =
    10.6    let
    10.7 -    val thy = ProofContext.theory_of lthy;
    10.8      val overloading = get_overloading lthy;
    10.9      fun pr_operation ((c, ty), (v, _)) =
   10.10 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
   10.11 -        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
   10.12 +      Pretty.block (Pretty.breaks
   10.13 +        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
   10.14 +          Pretty.str "::", Syntax.pretty_typ lthy ty]);
   10.15    in Pretty.str "overloading" :: map pr_operation overloading end;
   10.16  
   10.17  fun conclude lthy =
    11.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 13:48:45 2011 +0200
    11.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 15:25:25 2011 +0200
    11.3 @@ -37,6 +37,15 @@
    11.4    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    11.5    val facts_of: Proof.context -> Facts.T
    11.6    val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
    11.7 +  val class_space: Proof.context -> Name_Space.T
    11.8 +  val type_space: Proof.context -> Name_Space.T
    11.9 +  val const_space: Proof.context -> Name_Space.T
   11.10 +  val intern_class: Proof.context -> xstring -> string
   11.11 +  val intern_type: Proof.context -> xstring -> string
   11.12 +  val intern_const: Proof.context -> xstring -> string
   11.13 +  val extern_class: Proof.context -> string -> xstring
   11.14 +  val extern_type: Proof.context -> string -> xstring
   11.15 +  val extern_const: Proof.context -> string -> xstring
   11.16    val transfer_syntax: theory -> Proof.context -> Proof.context
   11.17    val transfer: theory -> Proof.context -> Proof.context
   11.18    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
   11.19 @@ -269,6 +278,21 @@
   11.20  val cases_of = #cases o rep_context;
   11.21  
   11.22  
   11.23 +(* name spaces *)
   11.24 +
   11.25 +val class_space = Type.class_space o tsig_of;
   11.26 +val type_space = Type.type_space o tsig_of;
   11.27 +val const_space = Consts.space_of o consts_of;
   11.28 +
   11.29 +val intern_class = Name_Space.intern o class_space;
   11.30 +val intern_type = Name_Space.intern o type_space;
   11.31 +val intern_const = Name_Space.intern o const_space;
   11.32 +
   11.33 +fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
   11.34 +fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
   11.35 +fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
   11.36 +
   11.37 +
   11.38  (* theory transfer *)
   11.39  
   11.40  fun transfer_syntax thy ctxt = ctxt |>
   11.41 @@ -351,7 +375,7 @@
   11.42  
   11.43  in
   11.44  
   11.45 -val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
   11.46 +val read_arity = prep_arity intern_type Syntax.read_sort;
   11.47  val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
   11.48  
   11.49  end;
   11.50 @@ -452,7 +476,7 @@
   11.51        TFree (c, default_sort ctxt (c, ~1)))
   11.52      else
   11.53        let
   11.54 -        val d = Type.intern_type tsig c;
   11.55 +        val d = intern_type ctxt c;
   11.56          val decl = Type.the_decl tsig d;
   11.57          val _ = Context_Position.report ctxt pos (Markup.tycon d);
   11.58          fun err () = error ("Bad type name: " ^ quote d);
    12.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 13:48:45 2011 +0200
    12.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 15:25:25 2011 +0200
    12.3 @@ -605,8 +605,6 @@
    12.4  fun unparse_t t_to_ast prt_t markup ctxt t =
    12.5    let
    12.6      val syn = ProofContext.syn_of ctxt;
    12.7 -    val tsig = ProofContext.tsig_of ctxt;
    12.8 -    val consts = ProofContext.consts_of ctxt;
    12.9  
   12.10      fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
   12.11        | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
   12.12 @@ -622,9 +620,9 @@
   12.13          SOME "" => ([], c)
   12.14        | SOME b => markup_extern b
   12.15        | NONE => c |> Lexicon.unmark
   12.16 -         {case_class = fn x => ([Markup.tclass x], Type.extern_class ctxt tsig x),
   12.17 -          case_type = fn x => ([Markup.tycon x], Type.extern_type ctxt tsig x),
   12.18 -          case_const = fn x => ([Markup.const x], Consts.extern ctxt consts x),
   12.19 +         {case_class = fn x => ([Markup.tclass x], ProofContext.extern_class ctxt x),
   12.20 +          case_type = fn x => ([Markup.tycon x], ProofContext.extern_type ctxt x),
   12.21 +          case_const = fn x => ([Markup.const x], ProofContext.extern_const ctxt x),
   12.22            case_fixed = fn x => free_or_skolem ctxt x,
   12.23            case_default = fn x => ([], x)});
   12.24    in
    13.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 16 13:48:45 2011 +0200
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 16 15:25:25 2011 +0200
    13.3 @@ -510,11 +510,11 @@
    13.4    in ProofContext.pretty_term_abbrev ctxt' eq end;
    13.5  
    13.6  fun pretty_class ctxt =
    13.7 -  Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
    13.8 +  Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt;
    13.9  
   13.10  fun pretty_type ctxt s =
   13.11    let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
   13.12 -  in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end;
   13.13 +  in Pretty.str (ProofContext.extern_type ctxt name) end;
   13.14  
   13.15  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
   13.16  
    14.1 --- a/src/Pure/display.ML	Sat Apr 16 13:48:45 2011 +0200
    14.2 +++ b/src/Pure/display.ML	Sat Apr 16 15:25:25 2011 +0200
    14.3 @@ -195,7 +195,7 @@
    14.4  
    14.5      val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
    14.6      val tdecls = Name_Space.dest_table ctxt types;
    14.7 -    val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities);
    14.8 +    val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
    14.9  
   14.10      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
   14.11      val cnsts = Name_Space.extern_table ctxt (#1 constants,
    15.1 --- a/src/Pure/sign.ML	Sat Apr 16 13:48:45 2011 +0200
    15.2 +++ b/src/Pure/sign.ML	Sat Apr 16 15:25:25 2011 +0200
    15.3 @@ -49,15 +49,12 @@
    15.4    val class_space: theory -> Name_Space.T
    15.5    val type_space: theory -> Name_Space.T
    15.6    val const_space: theory -> Name_Space.T
    15.7 +  val intern_class: theory -> xstring -> string
    15.8 +  val intern_type: theory -> xstring -> string
    15.9 +  val intern_const: theory -> xstring -> string
   15.10    val class_alias: binding -> class -> theory -> theory
   15.11    val type_alias: binding -> string -> theory -> theory
   15.12    val const_alias: binding -> string -> theory -> theory
   15.13 -  val intern_class: theory -> xstring -> string
   15.14 -  val extern_class: theory -> string -> xstring
   15.15 -  val intern_type: theory -> xstring -> string
   15.16 -  val extern_type: theory -> string -> xstring
   15.17 -  val intern_const: theory -> xstring -> string
   15.18 -  val extern_const: theory -> string -> xstring
   15.19    val arity_number: theory -> string -> int
   15.20    val arity_sorts: theory -> string -> sort -> sort list
   15.21    val certify_class: theory -> class -> class
   15.22 @@ -222,23 +219,20 @@
   15.23  
   15.24  
   15.25  
   15.26 -(** intern / extern names **)
   15.27 +(** name spaces **)
   15.28  
   15.29  val class_space = Type.class_space o tsig_of;
   15.30  val type_space = Type.type_space o tsig_of;
   15.31  val const_space = Consts.space_of o consts_of;
   15.32  
   15.33 +val intern_class = Name_Space.intern o class_space;
   15.34 +val intern_type = Name_Space.intern o type_space;
   15.35 +val intern_const = Name_Space.intern o const_space;
   15.36 +
   15.37  fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
   15.38  fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
   15.39  fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
   15.40  
   15.41 -val intern_class = Name_Space.intern o class_space;
   15.42 -fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy);
   15.43 -val intern_type = Name_Space.intern o type_space;
   15.44 -fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy);
   15.45 -val intern_const = Name_Space.intern o const_space;
   15.46 -fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy);
   15.47 -
   15.48  
   15.49  
   15.50  (** certify entities **)    (*exception TYPE*)
    16.1 --- a/src/Tools/Code/code_runtime.ML	Sat Apr 16 13:48:45 2011 +0200
    16.2 +++ b/src/Tools/Code/code_runtime.ML	Sat Apr 16 15:25:25 2011 +0200
    16.3 @@ -188,19 +188,23 @@
    16.4  
    16.5  fun evaluation_code thy module_name tycos consts =
    16.6    let
    16.7 +    val ctxt = ProofContext.init_global thy;
    16.8      val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
    16.9      val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
   16.10 -    val (ml_code, target_names) = Code_Target.produce_code_for thy
   16.11 -      target NONE module_name [] naming program (consts' @ tycos');
   16.12 +    val (ml_code, target_names) =
   16.13 +      Code_Target.produce_code_for thy
   16.14 +        target NONE module_name [] naming program (consts' @ tycos');
   16.15      val (consts'', tycos'') = chop (length consts') target_names;
   16.16 -    val consts_map = map2 (fn const => fn NONE =>
   16.17 -        error ("Constant " ^ (quote o Code.string_of_const thy) const
   16.18 -          ^ "\nhas a user-defined serialization")
   16.19 -      | SOME const'' => (const, const'')) consts consts''
   16.20 -    val tycos_map = map2 (fn tyco => fn NONE =>
   16.21 -        error ("Type " ^ (quote o Sign.extern_type thy) tyco
   16.22 -          ^ "\nhas a user-defined serialization")
   16.23 -      | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
   16.24 +    val consts_map = map2 (fn const =>
   16.25 +      fn NONE =>
   16.26 +          error ("Constant " ^ (quote o Code.string_of_const thy) const ^
   16.27 +            "\nhas a user-defined serialization")
   16.28 +       | SOME const'' => (const, const'')) consts consts''
   16.29 +    val tycos_map = map2 (fn tyco =>
   16.30 +      fn NONE =>
   16.31 +          error ("Type " ^ quote (ProofContext.extern_type ctxt tyco) ^
   16.32 +            "\nhas a user-defined serialization")
   16.33 +        | SOME tyco'' => (tyco, tyco'')) tycos tycos'';
   16.34    in (ml_code, (tycos_map, consts_map)) end;
   16.35  
   16.36  
    17.1 --- a/src/Tools/Code/code_target.ML	Sat Apr 16 13:48:45 2011 +0200
    17.2 +++ b/src/Tools/Code/code_target.ML	Sat Apr 16 15:25:25 2011 +0200
    17.3 @@ -307,13 +307,16 @@
    17.4  
    17.5  fun project_program thy abortable names_hidden names1 program2 =
    17.6    let
    17.7 +    val ctxt = ProofContext.init_global thy;
    17.8      val names2 = subtract (op =) names_hidden names1;
    17.9      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
   17.10      val names4 = Graph.all_succs program3 names2;
   17.11      val empty_funs = filter_out (member (op =) abortable)
   17.12        (Code_Thingol.empty_funs program3);
   17.13 -    val _ = if null empty_funs then () else error ("No code equations for "
   17.14 -      ^ commas (map (Sign.extern_const thy) empty_funs));
   17.15 +    val _ =
   17.16 +      if null empty_funs then ()
   17.17 +      else error ("No code equations for " ^
   17.18 +        commas (map (ProofContext.extern_const ctxt) empty_funs));
   17.19      val program4 = Graph.subgraph (member (op =) names4) program3;
   17.20    in (names4, program4) end;
   17.21  
    18.1 --- a/src/Tools/Code/code_thingol.ML	Sat Apr 16 13:48:45 2011 +0200
    18.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Apr 16 15:25:25 2011 +0200
    18.3 @@ -489,20 +489,29 @@
    18.4        end
    18.5    | _ => [];
    18.6  
    18.7 -fun labelled_name thy program name = case Graph.get_node program name
    18.8 - of Fun (c, _) => quote (Code.string_of_const thy c)
    18.9 -  | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco)
   18.10 -  | Datatypecons (c, _) => quote (Code.string_of_const thy c)
   18.11 -  | Class (class, _) => "class " ^ quote (Sign.extern_class thy class)
   18.12 -  | Classrel (sub, super) => let
   18.13 -        val Class (sub, _) = Graph.get_node program sub
   18.14 -        val Class (super, _) = Graph.get_node program super
   18.15 -      in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end
   18.16 -  | Classparam (c, _) => quote (Code.string_of_const thy c)
   18.17 -  | Classinst ((class, (tyco, _)), _) => let
   18.18 -        val Class (class, _) = Graph.get_node program class
   18.19 -        val Datatype (tyco, _) = Graph.get_node program tyco
   18.20 -      in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
   18.21 +fun labelled_name thy program name =
   18.22 +  let val ctxt = ProofContext.init_global thy in
   18.23 +    case Graph.get_node program name of
   18.24 +      Fun (c, _) => quote (Code.string_of_const thy c)
   18.25 +    | Datatype (tyco, _) => "type " ^ quote (ProofContext.extern_type ctxt tyco)
   18.26 +    | Datatypecons (c, _) => quote (Code.string_of_const thy c)
   18.27 +    | Class (class, _) => "class " ^ quote (ProofContext.extern_class ctxt class)
   18.28 +    | Classrel (sub, super) =>
   18.29 +        let
   18.30 +          val Class (sub, _) = Graph.get_node program sub;
   18.31 +          val Class (super, _) = Graph.get_node program super;
   18.32 +        in
   18.33 +          quote (ProofContext.extern_class ctxt sub ^ " < " ^ ProofContext.extern_class ctxt super)
   18.34 +        end
   18.35 +    | Classparam (c, _) => quote (Code.string_of_const thy c)
   18.36 +    | Classinst ((class, (tyco, _)), _) =>
   18.37 +        let
   18.38 +          val Class (class, _) = Graph.get_node program class;
   18.39 +          val Datatype (tyco, _) = Graph.get_node program tyco;
   18.40 +        in
   18.41 +          quote (ProofContext.extern_type ctxt tyco ^ " :: " ^ ProofContext.extern_class ctxt class)
   18.42 +        end
   18.43 +  end;
   18.44  
   18.45  fun linear_stmts program =
   18.46    rev (Graph.strong_conn program)
    19.1 --- a/src/ZF/Tools/inductive_package.ML	Sat Apr 16 13:48:45 2011 +0200
    19.2 +++ b/src/ZF/Tools/inductive_package.ML	Sat Apr 16 15:25:25 2011 +0200
    19.3 @@ -143,7 +143,7 @@
    19.4      If no mutual recursion then it equals the one recursive set.
    19.5      If mutual recursion then it differs from all the recursive sets. *)
    19.6    val big_rec_base_name = space_implode "_" rec_base_names;
    19.7 -  val big_rec_name = Sign.intern_const thy big_rec_base_name;
    19.8 +  val big_rec_name = ProofContext.intern_const ctxt big_rec_base_name;
    19.9  
   19.10  
   19.11    val _ =