tuned signature: eliminated pointless type Context.pretty;
authorwenzelm
Fri Sep 25 19:13:47 2015 +0200 (2015-09-25)
changeset 612627bd1eb4b056e
parent 61261 ddb2da7cb2e4
child 61263 48ab72301c1e
tuned signature: eliminated pointless type Context.pretty;
src/Pure/Isar/class.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax.ML
src/Pure/Tools/class_deps.ML
src/Pure/axclass.ML
src/Pure/consts.ML
src/Pure/context.ML
src/Pure/defs.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
src/Pure/sign.ML
src/Pure/sorts.ML
src/Pure/theory.ML
src/Pure/type.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Sep 24 23:33:29 2015 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Sep 25 19:13:47 2015 +0200
     1.3 @@ -599,7 +599,7 @@
     1.4                fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
     1.5        | matchings _ = I;
     1.6      val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
     1.7 -      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
     1.8 +      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
     1.9      val inst = map_type_tvar
    1.10        (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
    1.11    in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
    1.12 @@ -657,7 +657,7 @@
    1.13      val primary_constraints = map (apsnd
    1.14        (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
    1.15      val algebra = Sign.classes_of thy
    1.16 -      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
    1.17 +      |> fold (fn tyco => Sorts.add_arities (Context.Theory thy)
    1.18              (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
    1.19      val consts = Sign.consts_of thy;
    1.20      val improve_constraints = AList.lookup (op =)
     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 24 23:33:29 2015 +0200
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 25 19:13:47 2015 +0200
     2.3 @@ -287,7 +287,7 @@
     2.4  val tsig_of = #1 o #tsig o rep_data;
     2.5  val set_defsort = map_tsig o apfst o Type.set_defsort;
     2.6  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
     2.7 -fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
     2.8 +fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
     2.9  
    2.10  val consts_of = #1 o #consts o rep_data;
    2.11  val cases_of = #cases o rep_data;
    2.12 @@ -349,7 +349,7 @@
    2.13    map_tsig (fn tsig as (local_tsig, global_tsig) =>
    2.14      let val thy_tsig = Sign.tsig_of thy in
    2.15        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
    2.16 -      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
    2.17 +      else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
    2.18      end) |>
    2.19    map_consts (fn consts as (local_consts, global_consts) =>
    2.20      let val thy_consts = Sign.consts_of thy in
    2.21 @@ -555,7 +555,7 @@
    2.22  
    2.23  fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
    2.24    let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
    2.25 -  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
    2.26 +  in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
    2.27  
    2.28  in
    2.29  
    2.30 @@ -580,8 +580,9 @@
    2.31  
    2.32  local
    2.33  
    2.34 -fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
    2.35 -  (not (abbrev_mode ctxt)) (consts_of ctxt);
    2.36 +fun certify_consts ctxt =
    2.37 +  Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
    2.38 +    (not (abbrev_mode ctxt)) (consts_of ctxt);
    2.39  
    2.40  fun expand_binds ctxt =
    2.41    let
    2.42 @@ -764,7 +765,7 @@
    2.43    t
    2.44    |> expand_abbrevs ctxt
    2.45    |> (fn t' =>
    2.46 -      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    2.47 +      #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
    2.48          handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
    2.49  
    2.50  in
     3.1 --- a/src/Pure/Syntax/syntax.ML	Thu Sep 24 23:33:29 2015 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Sep 25 19:13:47 2015 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4    val is_pretty_global: Proof.context -> bool
     3.5    val set_pretty_global: bool -> Proof.context -> Proof.context
     3.6    val init_pretty_global: theory -> Proof.context
     3.7 -  val init_pretty: Context.pretty -> Proof.context
     3.8 +  val init_pretty: Context.generic -> Proof.context
     3.9    val pretty_term_global: theory -> term -> Pretty.T
    3.10    val pretty_typ_global: theory -> typ -> Pretty.T
    3.11    val pretty_sort_global: theory -> sort -> Pretty.T
    3.12 @@ -324,7 +324,7 @@
    3.13  fun is_pretty_global ctxt = Config.get ctxt pretty_global;
    3.14  val set_pretty_global = Config.put pretty_global;
    3.15  val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
    3.16 -val init_pretty = Context.pretty_context init_pretty_global;
    3.17 +val init_pretty = Context.cases init_pretty_global I;
    3.18  
    3.19  val pretty_term_global = pretty_term o init_pretty_global;
    3.20  val pretty_typ_global = pretty_typ o init_pretty_global;
     4.1 --- a/src/Pure/Tools/class_deps.ML	Thu Sep 24 23:33:29 2015 +0200
     4.2 +++ b/src/Pure/Tools/class_deps.ML	Fri Sep 25 19:13:47 2015 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4        Graph_Display.content_node (Name_Space.extern ctxt space c)
     4.5          (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
     4.6    in
     4.7 -    Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
     4.8 +    Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra
     4.9      |> #2 |> Sorts.classes_of |> Graph.dest
    4.10      |> map (fn ((c, _), ds) => ((c, node c), ds))
    4.11    end;
     5.1 --- a/src/Pure/axclass.ML	Thu Sep 24 23:33:29 2015 +0200
     5.2 +++ b/src/Pure/axclass.ML	Fri Sep 25 19:13:47 2015 +0200
     5.3 @@ -82,25 +82,25 @@
     5.4    Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
     5.5      proven_arities = proven_arities, inst_params = inst_params};
     5.6  
     5.7 -structure Data = Theory_Data_PP
     5.8 +structure Data = Theory_Data'
     5.9  (
    5.10    type T = data;
    5.11    val empty =
    5.12      make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty));
    5.13    val extend = I;
    5.14 -  fun merge pp
    5.15 +  fun merge old_thys
    5.16        (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
    5.17          proven_arities = proven_arities1, inst_params = inst_params1},
    5.18         Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
    5.19          proven_arities = proven_arities2, inst_params = inst_params2}) =
    5.20      let
    5.21 -      val ctxt = Syntax.init_pretty pp;
    5.22 +      val old_ctxt = Syntax.init_pretty_global (fst old_thys);
    5.23  
    5.24        val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
    5.25        val params' =
    5.26          if null params1 then params2
    5.27          else
    5.28 -          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
    5.29 +          fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
    5.30              params2 params1;
    5.31  
    5.32        (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
     6.1 --- a/src/Pure/consts.ML	Thu Sep 24 23:33:29 2015 +0200
     6.2 +++ b/src/Pure/consts.ML	Fri Sep 25 19:13:47 2015 +0200
     6.3 @@ -27,7 +27,7 @@
     6.4    val intern: T -> xstring -> string
     6.5    val intern_syntax: T -> xstring -> string
     6.6    val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
     6.7 -  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     6.8 +  val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     6.9    val typargs: T -> string * typ -> typ list
    6.10    val instance: T -> string * typ list -> typ
    6.11    val declare: Context.generic -> binding * typ -> T -> T
    6.12 @@ -155,11 +155,11 @@
    6.13  
    6.14  (* certify *)
    6.15  
    6.16 -fun certify pp tsig do_expand consts =
    6.17 +fun certify context tsig do_expand consts =
    6.18    let
    6.19      fun err msg (c, T) =
    6.20        raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
    6.21 -        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
    6.22 +        Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
    6.23      val certT = Type.cert_typ tsig;
    6.24      fun cert tm =
    6.25        let
    6.26 @@ -272,9 +272,8 @@
    6.27  
    6.28  fun abbreviate context tsig mode (b, raw_rhs) consts =
    6.29    let
    6.30 -    val pp = Context.pretty_generic context;
    6.31 -    val cert_term = certify pp tsig false consts;
    6.32 -    val expand_term = certify pp tsig true consts;
    6.33 +    val cert_term = certify context tsig false consts;
    6.34 +    val expand_term = certify context tsig true consts;
    6.35      val force_expand = mode = Print_Mode.internal;
    6.36  
    6.37      val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
     7.1 --- a/src/Pure/context.ML	Thu Sep 24 23:33:29 2015 +0200
     7.2 +++ b/src/Pure/context.ML	Fri Sep 25 19:13:47 2015 +0200
     7.3 @@ -31,7 +31,6 @@
     7.4    type theory_id
     7.5    val theory_id: theory -> theory_id
     7.6    val timing: bool Unsynchronized.ref
     7.7 -  type pretty
     7.8    val parents_of: theory -> theory list
     7.9    val ancestors_of: theory -> theory list
    7.10    val theory_id_name: theory_id -> string
    7.11 @@ -52,7 +51,7 @@
    7.12    val subthy_id: theory_id * theory_id -> bool
    7.13    val subthy: theory * theory -> bool
    7.14    val finish_thy: theory -> theory
    7.15 -  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
    7.16 +  val begin_thy: string -> theory list -> theory
    7.17    (*proof context*)
    7.18    val raw_transfer: theory -> Proof.context -> Proof.context
    7.19    (*certificate*)
    7.20 @@ -77,11 +76,6 @@
    7.21    val proof_map: (generic -> generic) -> Proof.context -> Proof.context
    7.22    val theory_of: generic -> theory  (*total*)
    7.23    val proof_of: generic -> Proof.context  (*total*)
    7.24 -  (*pretty printing context*)
    7.25 -  val pretty: Proof.context -> pretty
    7.26 -  val pretty_global: theory -> pretty
    7.27 -  val pretty_generic: generic -> pretty
    7.28 -  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
    7.29    (*thread data*)
    7.30    val thread_data: unit -> generic option
    7.31    val the_thread_data: unit -> generic
    7.32 @@ -97,7 +91,7 @@
    7.33    structure Theory_Data:
    7.34    sig
    7.35      val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
    7.36 -      (pretty -> Any.T * Any.T -> Any.T) -> serial
    7.37 +      (theory * theory -> Any.T * Any.T -> Any.T) -> serial
    7.38      val get: serial -> (Any.T -> 'a) -> theory -> 'a
    7.39      val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
    7.40    end
    7.41 @@ -114,55 +108,9 @@
    7.42  
    7.43  (*** theory context ***)
    7.44  
    7.45 -(** theory data **)
    7.46 -
    7.47 -(* data kinds and access methods *)
    7.48 -
    7.49 -val timing = Unsynchronized.ref false;
    7.50 -
    7.51  (*private copy avoids potential conflict of table exceptions*)
    7.52  structure Datatab = Table(type key = int val ord = int_ord);
    7.53  
    7.54 -datatype pretty = Pretty of Any.T;
    7.55 -
    7.56 -local
    7.57 -
    7.58 -type kind =
    7.59 - {pos: Position.T,
    7.60 -  empty: Any.T,
    7.61 -  extend: Any.T -> Any.T,
    7.62 -  merge: pretty -> Any.T * Any.T -> Any.T};
    7.63 -
    7.64 -val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
    7.65 -
    7.66 -fun invoke name f k x =
    7.67 -  (case Datatab.lookup (Synchronized.value kinds) k of
    7.68 -    SOME kind =>
    7.69 -      if ! timing andalso name <> "" then
    7.70 -        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
    7.71 -          (fn () => f kind x)
    7.72 -      else f kind x
    7.73 -  | NONE => raise Fail "Invalid theory data identifier");
    7.74 -
    7.75 -in
    7.76 -
    7.77 -fun invoke_empty k = invoke "" (K o #empty) k ();
    7.78 -val invoke_extend = invoke "extend" #extend;
    7.79 -fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
    7.80 -
    7.81 -fun declare_theory_data pos empty extend merge =
    7.82 -  let
    7.83 -    val k = serial ();
    7.84 -    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
    7.85 -    val _ = Synchronized.change kinds (Datatab.update (k, kind));
    7.86 -  in k end;
    7.87 -
    7.88 -val extend_data = Datatab.map invoke_extend;
    7.89 -fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
    7.90 -
    7.91 -end;
    7.92 -
    7.93 -
    7.94  
    7.95  (** datatype theory **)
    7.96  
    7.97 @@ -288,6 +236,51 @@
    7.98  
    7.99  
   7.100  
   7.101 +(** theory data **)
   7.102 +
   7.103 +(* data kinds and access methods *)
   7.104 +
   7.105 +val timing = Unsynchronized.ref false;
   7.106 +
   7.107 +local
   7.108 +
   7.109 +type kind =
   7.110 + {pos: Position.T,
   7.111 +  empty: Any.T,
   7.112 +  extend: Any.T -> Any.T,
   7.113 +  merge: theory * theory -> Any.T * Any.T -> Any.T};
   7.114 +
   7.115 +val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
   7.116 +
   7.117 +fun invoke name f k x =
   7.118 +  (case Datatab.lookup (Synchronized.value kinds) k of
   7.119 +    SOME kind =>
   7.120 +      if ! timing andalso name <> "" then
   7.121 +        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
   7.122 +          (fn () => f kind x)
   7.123 +      else f kind x
   7.124 +  | NONE => raise Fail "Invalid theory data identifier");
   7.125 +
   7.126 +in
   7.127 +
   7.128 +fun invoke_empty k = invoke "" (K o #empty) k ();
   7.129 +val invoke_extend = invoke "extend" #extend;
   7.130 +fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
   7.131 +
   7.132 +fun declare_theory_data pos empty extend merge =
   7.133 +  let
   7.134 +    val k = serial ();
   7.135 +    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
   7.136 +    val _ = Synchronized.change kinds (Datatab.update (k, kind));
   7.137 +  in k end;
   7.138 +
   7.139 +val extend_data = Datatab.map invoke_extend;
   7.140 +fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
   7.141 +
   7.142 +end;
   7.143 +
   7.144 +
   7.145 +
   7.146  (** build theories **)
   7.147  
   7.148  (* primitives *)
   7.149 @@ -325,12 +318,12 @@
   7.150  
   7.151  local
   7.152  
   7.153 -fun merge_thys pp (thy1, thy2) =
   7.154 +fun merge_thys (thy1, thy2) =
   7.155    let
   7.156      val ids = merge_ids thy1 thy2;
   7.157      val history = make_history "" 0;
   7.158      val ancestry = make_ancestry [] [];
   7.159 -    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   7.160 +    val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
   7.161    in create_thy ids history ancestry data end;
   7.162  
   7.163  fun maximal_thys thys =
   7.164 @@ -338,7 +331,7 @@
   7.165  
   7.166  in
   7.167  
   7.168 -fun begin_thy pp name imports =
   7.169 +fun begin_thy name imports =
   7.170    if name = "" then error ("Bad theory name: " ^ quote name)
   7.171    else
   7.172      let
   7.173 @@ -351,7 +344,7 @@
   7.174          (case parents of
   7.175            [] => error "Missing theory imports"
   7.176          | [thy] => extend_thy thy
   7.177 -        | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
   7.178 +        | thy :: thys => Library.foldl merge_thys (thy, thys));
   7.179  
   7.180        val history = make_history name 0;
   7.181        val ancestry = make_ancestry parents ancestors;
   7.182 @@ -498,17 +491,6 @@
   7.183  val proof_of = cases Proof_Context.init_global I;
   7.184  
   7.185  
   7.186 -(* pretty printing context *)
   7.187 -
   7.188 -exception PRETTY of generic;
   7.189 -
   7.190 -val pretty_generic = Pretty o PRETTY;
   7.191 -val pretty = pretty_generic o Proof;
   7.192 -val pretty_global = pretty_generic o Theory;
   7.193 -
   7.194 -fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
   7.195 -
   7.196 -
   7.197  
   7.198  (** thread data **)
   7.199  
   7.200 @@ -551,12 +533,12 @@
   7.201  
   7.202  (** theory data **)
   7.203  
   7.204 -signature THEORY_DATA_PP_ARGS =
   7.205 +signature THEORY_DATA'_ARGS =
   7.206  sig
   7.207    type T
   7.208    val empty: T
   7.209    val extend: T -> T
   7.210 -  val merge: Context.pretty -> T * T -> T
   7.211 +  val merge: theory * theory -> T * T -> T
   7.212  end;
   7.213  
   7.214  signature THEORY_DATA_ARGS =
   7.215 @@ -575,7 +557,7 @@
   7.216    val map: (T -> T) -> theory -> theory
   7.217  end;
   7.218  
   7.219 -functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
   7.220 +functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
   7.221  struct
   7.222  
   7.223  type T = Data.T;
   7.224 @@ -586,7 +568,7 @@
   7.225      (Position.thread_data ())
   7.226      (Data Data.empty)
   7.227      (fn Data x => Data (Data.extend x))
   7.228 -    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
   7.229 +    (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
   7.230  
   7.231  val get = Context.Theory_Data.get kind (fn Data x => x);
   7.232  val put = Context.Theory_Data.put kind Data;
   7.233 @@ -595,7 +577,7 @@
   7.234  end;
   7.235  
   7.236  functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
   7.237 -  Theory_Data_PP
   7.238 +  Theory_Data'
   7.239    (
   7.240      type T = Data.T;
   7.241      val empty = Data.empty;
     8.1 --- a/src/Pure/defs.ML	Thu Sep 24 23:33:29 2015 +0200
     8.2 +++ b/src/Pure/defs.ML	Fri Sep 25 19:13:47 2015 +0200
     8.3 @@ -13,6 +13,7 @@
     8.4    val item_kind_ord: item_kind * item_kind -> order
     8.5    val plain_args: typ list -> bool
     8.6    type context = Proof.context * (Name_Space.T * Name_Space.T) option
     8.7 +  val global_context: theory -> context
     8.8    val space: context -> item_kind -> Name_Space.T
     8.9    val pretty_item: context -> item -> Pretty.T
    8.10    val pretty_args: Proof.context -> typ list -> Pretty.T list
    8.11 @@ -55,6 +56,8 @@
    8.12  
    8.13  type context = Proof.context * (Name_Space.T * Name_Space.T) option;
    8.14  
    8.15 +fun global_context thy : context = (Syntax.init_pretty_global thy, NONE);
    8.16 +
    8.17  fun space (ctxt, spaces) kind =
    8.18    (case (kind, spaces) of
    8.19      (Const, SOME (const_space, _)) => const_space
     9.1 --- a/src/Pure/global_theory.ML	Thu Sep 24 23:33:29 2015 +0200
     9.2 +++ b/src/Pure/global_theory.ML	Fri Sep 25 19:13:47 2015 +0200
     9.3 @@ -205,9 +205,9 @@
     9.4  
     9.5  fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
     9.6    let
     9.7 -    val ctxt = Syntax.init_pretty_global thy;
     9.8 +    val context as (ctxt, _) = Defs.global_context thy;
     9.9      val prop = prep ctxt (b, raw_prop);
    9.10 -    val ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy;
    9.11 +    val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
    9.12      val thm = def
    9.13        |> Thm.forall_intr_frees
    9.14        |> Thm.forall_elim_vars 0
    10.1 --- a/src/Pure/more_thm.ML	Thu Sep 24 23:33:29 2015 +0200
    10.2 +++ b/src/Pure/more_thm.ML	Fri Sep 25 19:13:47 2015 +0200
    10.3 @@ -491,7 +491,7 @@
    10.4    in ((axm_name, thm), thy') end;
    10.5  
    10.6  fun add_def_global unchecked overloaded arg thy =
    10.7 -  add_def (Syntax.init_pretty_global thy, NONE) unchecked overloaded arg thy;
    10.8 +  add_def (Defs.global_context thy) unchecked overloaded arg thy;
    10.9  
   10.10  
   10.11  
    11.1 --- a/src/Pure/sign.ML	Thu Sep 24 23:33:29 2015 +0200
    11.2 +++ b/src/Pure/sign.ML	Fri Sep 25 19:13:47 2015 +0200
    11.3 @@ -62,7 +62,7 @@
    11.4    val certify_sort: theory -> sort -> sort
    11.5    val certify_typ: theory -> typ -> typ
    11.6    val certify_typ_mode: Type.mode -> theory -> typ -> typ
    11.7 -  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
    11.8 +  val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
    11.9    val certify_term: theory -> term -> term * typ * int
   11.10    val cert_term: theory -> term -> term
   11.11    val cert_prop: theory -> term -> term
   11.12 @@ -133,20 +133,20 @@
   11.13  
   11.14  fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
   11.15  
   11.16 -structure Data = Theory_Data_PP
   11.17 +structure Data = Theory_Data'
   11.18  (
   11.19    type T = sign;
   11.20    fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
   11.21  
   11.22    val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
   11.23  
   11.24 -  fun merge pp (sign1, sign2) =
   11.25 +  fun merge old_thys (sign1, sign2) =
   11.26      let
   11.27        val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
   11.28        val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
   11.29  
   11.30        val syn = Syntax.merge_syntax (syn1, syn2);
   11.31 -      val tsig = Type.merge_tsig pp (tsig1, tsig2);
   11.32 +      val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
   11.33        val consts = Consts.merge (consts1, consts2);
   11.34      in make_sign (syn, tsig, consts) end;
   11.35  );
   11.36 @@ -257,7 +257,7 @@
   11.37  (* certify wrt. type signature *)
   11.38  
   11.39  val arity_number = Type.arity_number o tsig_of;
   11.40 -fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
   11.41 +fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
   11.42  
   11.43  val certify_class = Type.cert_class o tsig_of;
   11.44  val certify_sort = Type.cert_sort o tsig_of;
   11.45 @@ -269,14 +269,14 @@
   11.46  
   11.47  local
   11.48  
   11.49 -fun type_check pp tm =
   11.50 +fun type_check context tm =
   11.51    let
   11.52      fun err_appl bs t T u U =
   11.53        let
   11.54          val xs = map Free bs;           (*we do not rename here*)
   11.55          val t' = subst_bounds (xs, t);
   11.56          val u' = subst_bounds (xs, u);
   11.57 -        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
   11.58 +        val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
   11.59        in raise TYPE (msg, [T, U], [t', u']) end;
   11.60  
   11.61      fun typ_of (_, Const (_, T)) = T
   11.62 @@ -306,20 +306,19 @@
   11.63  
   11.64  in
   11.65  
   11.66 -fun certify' prop pp do_expand consts thy tm =
   11.67 +fun certify' prop context do_expand consts thy tm =
   11.68    let
   11.69      val _ = check_vars tm;
   11.70      val tm' = Term.map_types (certify_typ thy) tm;
   11.71 -    val T = type_check pp tm';
   11.72 +    val T = type_check context tm';
   11.73      val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
   11.74 -    val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
   11.75 +    val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
   11.76    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
   11.77  
   11.78 -fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
   11.79 -fun cert_term_abbrev thy =
   11.80 -  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
   11.81 +fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
   11.82 +fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
   11.83  val cert_term = #1 oo certify_term;
   11.84 -fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
   11.85 +fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
   11.86  
   11.87  end;
   11.88  
   11.89 @@ -474,10 +473,10 @@
   11.90    |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   11.91  
   11.92  fun primitive_classrel arg thy =
   11.93 -  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
   11.94 +  thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
   11.95  
   11.96  fun primitive_arity arg thy =
   11.97 -  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
   11.98 +  thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
   11.99  
  11.100  
  11.101  (* add translation functions *)
    12.1 --- a/src/Pure/sorts.ML	Thu Sep 24 23:33:29 2015 +0200
    12.2 +++ b/src/Pure/sorts.ML	Fri Sep 25 19:13:47 2015 +0200
    12.3 @@ -38,15 +38,15 @@
    12.4    val minimize_sort: algebra -> sort -> sort
    12.5    val complete_sort: algebra -> sort -> sort
    12.6    val minimal_sorts: algebra -> sort list -> sort Ord_List.T
    12.7 -  val add_class: Context.pretty -> class * class list -> algebra -> algebra
    12.8 -  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
    12.9 -  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
   12.10 +  val add_class: Context.generic -> class * class list -> algebra -> algebra
   12.11 +  val add_classrel: Context.generic -> class * class -> algebra -> algebra
   12.12 +  val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
   12.13    val empty_algebra: algebra
   12.14 -  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
   12.15 -  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
   12.16 +  val merge_algebra: Context.generic -> algebra * algebra -> algebra
   12.17 +  val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option)
   12.18      -> algebra -> (sort -> sort) * algebra
   12.19    type class_error
   12.20 -  val class_error: Context.pretty -> class_error -> string
   12.21 +  val class_error: Context.generic -> class_error -> string
   12.22    exception CLASS_ERROR of class_error
   12.23    val has_instance: algebra -> string -> sort -> bool
   12.24    val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
    13.1 --- a/src/Pure/theory.ML	Thu Sep 24 23:33:29 2015 +0200
    13.2 +++ b/src/Pure/theory.ML	Fri Sep 25 19:13:47 2015 +0200
    13.3 @@ -64,7 +64,7 @@
    13.4  fun make_thy (pos, id, axioms, defs, wrappers) =
    13.5    Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
    13.6  
    13.7 -structure Thy = Theory_Data_PP
    13.8 +structure Thy = Theory_Data'
    13.9  (
   13.10    type T = thy;
   13.11    val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
   13.12 @@ -73,13 +73,13 @@
   13.13    fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
   13.14      make_thy (Position.none, 0, empty_axioms, defs, wrappers);
   13.15  
   13.16 -  fun merge pp (thy1, thy2) =
   13.17 +  fun merge old_thys (thy1, thy2) =
   13.18      let
   13.19        val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   13.20        val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   13.21  
   13.22        val axioms' = empty_axioms;
   13.23 -      val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2);
   13.24 +      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
   13.25        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   13.26        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   13.27      in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
   13.28 @@ -164,7 +164,7 @@
   13.29      | _ => error "Bad bootstrapping of theory Pure")
   13.30    else
   13.31      let
   13.32 -      val thy = Context.begin_thy Context.pretty_global name imports;
   13.33 +      val thy = Context.begin_thy name imports;
   13.34        val wrappers = begin_wrappers thy;
   13.35      in
   13.36        thy
   13.37 @@ -249,7 +249,7 @@
   13.38    in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
   13.39  
   13.40  fun add_deps_global a x y thy =
   13.41 -  add_deps (Syntax.init_pretty_global thy, NONE) a x y thy;
   13.42 +  add_deps (Defs.global_context thy) a x y thy;
   13.43  
   13.44  fun specify_const decl thy =
   13.45    let val (t, thy') = Sign.declare_const_global decl thy;
    14.1 --- a/src/Pure/type.ML	Thu Sep 24 23:33:29 2015 +0200
    14.2 +++ b/src/Pure/type.ML	Fri Sep 25 19:13:47 2015 +0200
    14.3 @@ -55,7 +55,7 @@
    14.4    val cert_typ_mode: mode -> tsig -> typ -> typ
    14.5    val cert_typ: tsig -> typ -> typ
    14.6    val arity_number: tsig -> string -> int
    14.7 -  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
    14.8 +  val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
    14.9  
   14.10    (*special treatment of type vars*)
   14.11    val sort_of_atyp: typ -> sort
   14.12 @@ -96,9 +96,9 @@
   14.13    val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
   14.14    val add_nonterminal: Context.generic -> binding -> tsig -> tsig
   14.15    val hide_type: bool -> string -> tsig -> tsig
   14.16 -  val add_arity: Context.pretty -> arity -> tsig -> tsig
   14.17 -  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
   14.18 -  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
   14.19 +  val add_arity: Context.generic -> arity -> tsig -> tsig
   14.20 +  val add_classrel: Context.generic -> class * class -> tsig -> tsig
   14.21 +  val merge_tsig: Context.generic -> tsig * tsig -> tsig
   14.22  end;
   14.23  
   14.24  structure Type: TYPE =
   14.25 @@ -321,9 +321,9 @@
   14.26    | _ => error (undecl_type a));
   14.27  
   14.28  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   14.29 -  | arity_sorts pp (TSig {classes, ...}) a S =
   14.30 +  | arity_sorts context (TSig {classes, ...}) a S =
   14.31        Sorts.mg_domain (#2 classes) a S
   14.32 -        handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
   14.33 +        handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err);
   14.34  
   14.35  
   14.36  
   14.37 @@ -609,7 +609,7 @@
   14.38          handle TYPE (msg, _, _) => error msg;
   14.39        val _ = Binding.check c;
   14.40        val (c', space') = space |> Name_Space.declare context true c;
   14.41 -      val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
   14.42 +      val classes' = classes |> Sorts.add_class context (c', cs');
   14.43      in ((space', classes'), default, types) end);
   14.44  
   14.45  fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
   14.46 @@ -618,7 +618,7 @@
   14.47  
   14.48  (* arities *)
   14.49  
   14.50 -fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   14.51 +fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   14.52    let
   14.53      val _ =
   14.54        (case lookup_type tsig t of
   14.55 @@ -627,18 +627,18 @@
   14.56        | NONE => error (undecl_type t));
   14.57      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   14.58        handle TYPE (msg, _, _) => error msg;
   14.59 -    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   14.60 +    val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S'));
   14.61    in ((space, classes'), default, types) end);
   14.62  
   14.63  
   14.64  (* classrel *)
   14.65  
   14.66 -fun add_classrel pp rel tsig =
   14.67 +fun add_classrel context rel tsig =
   14.68    tsig |> map_tsig (fn ((space, classes), default, types) =>
   14.69      let
   14.70        val rel' = apply2 (cert_class tsig) rel
   14.71          handle TYPE (msg, _, _) => error msg;
   14.72 -      val classes' = classes |> Sorts.add_classrel pp rel';
   14.73 +      val classes' = classes |> Sorts.add_classrel context rel';
   14.74      in ((space, classes'), default, types) end);
   14.75  
   14.76  
   14.77 @@ -701,7 +701,7 @@
   14.78  
   14.79  (* merge type signatures *)
   14.80  
   14.81 -fun merge_tsig pp (tsig1, tsig2) =
   14.82 +fun merge_tsig context (tsig1, tsig2) =
   14.83    let
   14.84      val (TSig {classes = (space1, classes1), default = default1, types = types1,
   14.85        log_types = _}) = tsig1;
   14.86 @@ -709,7 +709,7 @@
   14.87        log_types = _}) = tsig2;
   14.88  
   14.89      val space' = Name_Space.merge (space1, space2);
   14.90 -    val classes' = Sorts.merge_algebra pp (classes1, classes2);
   14.91 +    val classes' = Sorts.merge_algebra context (classes1, classes2);
   14.92      val default' = Sorts.inter_sort classes' (default1, default2);
   14.93      val types' = Name_Space.merge_tables (types1, types2);
   14.94    in build_tsig ((space', classes'), default', types') end;
    15.1 --- a/src/Tools/Code/code_preproc.ML	Thu Sep 24 23:33:29 2015 +0200
    15.2 +++ b/src/Tools/Code/code_preproc.ML	Fri Sep 25 19:13:47 2015 +0200
    15.3 @@ -517,7 +517,7 @@
    15.4        |> fold (ensure_fun ctxt arities eqngr) cs
    15.5        |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
    15.6      val arities' = fold (add_arity ctxt vardeps) insts arities;
    15.7 -    val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
    15.8 +    val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy)
    15.9        (AList.lookup (op =) arities') (Sign.classes_of thy);
   15.10      val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
   15.11      fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
    16.1 --- a/src/Tools/Code/code_thingol.ML	Thu Sep 24 23:33:29 2015 +0200
    16.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Sep 25 19:13:47 2015 +0200
    16.3 @@ -412,7 +412,7 @@
    16.4  
    16.5  fun not_wellsorted ctxt permissive some_thm deps ty sort e =
    16.6    let
    16.7 -    val err_class = Sorts.class_error (Context.pretty ctxt) e;
    16.8 +    val err_class = Sorts.class_error (Context.Proof ctxt) e;
    16.9      val err_typ =
   16.10        "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
   16.11          Syntax.string_of_sort ctxt sort;