# HG changeset patch
# User wenzelm
# Date 1443201227 -7200
# Node ID 7bd1eb4b056eea87f579a2d6a0fde707fcb363e5
# Parent  ddb2da7cb2e44042263714e97cfbe9944bda54a1
tuned signature: eliminated pointless type Context.pretty;

diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Isar/class.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -599,7 +599,7 @@
               fold2 (curry (Sorts.meet_sort algebra)) (Consts.typargs consts c_ty) sorts)
       | matchings _ = I;
     val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
-      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.pretty ctxt) e);
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error (Context.Proof ctxt) e);
     val inst = map_type_tvar
       (fn (vi, sort) => TVar (vi, the_default sort (Vartab.lookup tvartab vi)));
   in if Vartab.is_empty tvartab then ts else (map o map_types) inst ts end;
@@ -657,7 +657,7 @@
     val primary_constraints = map (apsnd
       (map_atyps (K (TVar ((Name.aT, 0), [])))) o snd o snd) class_params;
     val algebra = Sign.classes_of thy
-      |> fold (fn tyco => Sorts.add_arities (Context.pretty_global thy)
+      |> fold (fn tyco => Sorts.add_arities (Context.Theory thy)
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -287,7 +287,7 @@
 val tsig_of = #1 o #tsig o rep_data;
 val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
-fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
+fun arity_sorts ctxt = Type.arity_sorts (Context.Proof ctxt) (tsig_of ctxt);
 
 val consts_of = #1 o #consts o rep_data;
 val cases_of = #cases o rep_data;
@@ -349,7 +349,7 @@
   map_tsig (fn tsig as (local_tsig, global_tsig) =>
     let val thy_tsig = Sign.tsig_of thy in
       if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig (Context.pretty ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
+      else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
@@ -555,7 +555,7 @@
 
 fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
-  in Type.add_arity (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
+  in Type.add_arity (Context.Proof ctxt) arity (tsig_of ctxt); arity end;
 
 in
 
@@ -580,8 +580,9 @@
 
 local
 
-fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
-  (not (abbrev_mode ctxt)) (consts_of ctxt);
+fun certify_consts ctxt =
+  Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
+    (not (abbrev_mode ctxt)) (consts_of ctxt);
 
 fun expand_binds ctxt =
   let
@@ -764,7 +765,7 @@
   t
   |> expand_abbrevs ctxt
   |> (fn t' =>
-      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+      #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
         handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
 
 in
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -65,7 +65,7 @@
   val is_pretty_global: Proof.context -> bool
   val set_pretty_global: bool -> Proof.context -> Proof.context
   val init_pretty_global: theory -> Proof.context
-  val init_pretty: Context.pretty -> Proof.context
+  val init_pretty: Context.generic -> Proof.context
   val pretty_term_global: theory -> term -> Pretty.T
   val pretty_typ_global: theory -> typ -> Pretty.T
   val pretty_sort_global: theory -> sort -> Pretty.T
@@ -324,7 +324,7 @@
 fun is_pretty_global ctxt = Config.get ctxt pretty_global;
 val set_pretty_global = Config.put pretty_global;
 val init_pretty_global = set_pretty_global true o Proof_Context.init_global;
-val init_pretty = Context.pretty_context init_pretty_global;
+val init_pretty = Context.cases init_pretty_global I;
 
 val pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -29,7 +29,7 @@
       Graph_Display.content_node (Name_Space.extern ctxt space c)
         (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
   in
-    Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
+    Sorts.subalgebra (Context.Proof ctxt) pred (K NONE) algebra
     |> #2 |> Sorts.classes_of |> Graph.dest
     |> map (fn ((c, _), ds) => ((c, node c), ds))
   end;
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/axclass.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -82,25 +82,25 @@
   Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
     proven_arities = proven_arities, inst_params = inst_params};
 
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
 (
   type T = data;
   val empty =
     make_data (Symtab.empty, [], Symreltab.empty, Symtab.empty, (Symtab.empty, Symtab.empty));
   val extend = I;
-  fun merge pp
+  fun merge old_thys
       (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
         proven_arities = proven_arities1, inst_params = inst_params1},
        Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
         proven_arities = proven_arities2, inst_params = inst_params2}) =
     let
-      val ctxt = Syntax.init_pretty pp;
+      val old_ctxt = Syntax.init_pretty_global (fst old_thys);
 
       val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
       val params' =
         if null params1 then params2
         else
-          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+          fold_rev (fn p => if member (op =) params1 p then I else add_param old_ctxt p)
             params2 params1;
 
       (*see Theory.at_begin hook for transitive closure of classrels and arity completion*)
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/consts.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -27,7 +27,7 @@
   val intern: T -> xstring -> string
   val intern_syntax: T -> xstring -> string
   val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
-  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
+  val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: Context.generic -> binding * typ -> T -> T
@@ -155,11 +155,11 @@
 
 (* certify *)
 
-fun certify pp tsig do_expand consts =
+fun certify context tsig do_expand consts =
   let
     fun err msg (c, T) =
       raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
-        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
+        Syntax.string_of_typ (Syntax.init_pretty context) T, [], []);
     val certT = Type.cert_typ tsig;
     fun cert tm =
       let
@@ -272,9 +272,8 @@
 
 fun abbreviate context tsig mode (b, raw_rhs) consts =
   let
-    val pp = Context.pretty_generic context;
-    val cert_term = certify pp tsig false consts;
-    val expand_term = certify pp tsig true consts;
+    val cert_term = certify context tsig false consts;
+    val expand_term = certify context tsig true consts;
     val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/context.ML
--- a/src/Pure/context.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/context.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -31,7 +31,6 @@
   type theory_id
   val theory_id: theory -> theory_id
   val timing: bool Unsynchronized.ref
-  type pretty
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_name: theory_id -> string
@@ -52,7 +51,7 @@
   val subthy_id: theory_id * theory_id -> bool
   val subthy: theory * theory -> bool
   val finish_thy: theory -> theory
-  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
+  val begin_thy: string -> theory list -> theory
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*certificate*)
@@ -77,11 +76,6 @@
   val proof_map: (generic -> generic) -> Proof.context -> Proof.context
   val theory_of: generic -> theory  (*total*)
   val proof_of: generic -> Proof.context  (*total*)
-  (*pretty printing context*)
-  val pretty: Proof.context -> pretty
-  val pretty_global: theory -> pretty
-  val pretty_generic: generic -> pretty
-  val pretty_context: (theory -> Proof.context) -> pretty -> Proof.context
   (*thread data*)
   val thread_data: unit -> generic option
   val the_thread_data: unit -> generic
@@ -97,7 +91,7 @@
   structure Theory_Data:
   sig
     val declare: Position.T -> Any.T -> (Any.T -> Any.T) ->
-      (pretty -> Any.T * Any.T -> Any.T) -> serial
+      (theory * theory -> Any.T * Any.T -> Any.T) -> serial
     val get: serial -> (Any.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Any.T) -> 'a -> theory -> theory
   end
@@ -114,55 +108,9 @@
 
 (*** theory context ***)
 
-(** theory data **)
-
-(* data kinds and access methods *)
-
-val timing = Unsynchronized.ref false;
-
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
-datatype pretty = Pretty of Any.T;
-
-local
-
-type kind =
- {pos: Position.T,
-  empty: Any.T,
-  extend: Any.T -> Any.T,
-  merge: pretty -> Any.T * Any.T -> Any.T};
-
-val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
-
-fun invoke name f k x =
-  (case Datatab.lookup (Synchronized.value kinds) k of
-    SOME kind =>
-      if ! timing andalso name <> "" then
-        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
-          (fn () => f kind x)
-      else f kind x
-  | NONE => raise Fail "Invalid theory data identifier");
-
-in
-
-fun invoke_empty k = invoke "" (K o #empty) k ();
-val invoke_extend = invoke "extend" #extend;
-fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp);
-
-fun declare_theory_data pos empty extend merge =
-  let
-    val k = serial ();
-    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
-    val _ = Synchronized.change kinds (Datatab.update (k, kind));
-  in k end;
-
-val extend_data = Datatab.map invoke_extend;
-fun merge_data pp = Datatab.join (invoke_merge pp) o apply2 extend_data;
-
-end;
-
-
 
 (** datatype theory **)
 
@@ -288,6 +236,51 @@
 
 
 
+(** theory data **)
+
+(* data kinds and access methods *)
+
+val timing = Unsynchronized.ref false;
+
+local
+
+type kind =
+ {pos: Position.T,
+  empty: Any.T,
+  extend: Any.T -> Any.T,
+  merge: theory * theory -> Any.T * Any.T -> Any.T};
+
+val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
+
+fun invoke name f k x =
+  (case Datatab.lookup (Synchronized.value kinds) k of
+    SOME kind =>
+      if ! timing andalso name <> "" then
+        Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.here (#pos kind))
+          (fn () => f kind x)
+      else f kind x
+  | NONE => raise Fail "Invalid theory data identifier");
+
+in
+
+fun invoke_empty k = invoke "" (K o #empty) k ();
+val invoke_extend = invoke "extend" #extend;
+fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys);
+
+fun declare_theory_data pos empty extend merge =
+  let
+    val k = serial ();
+    val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
+    val _ = Synchronized.change kinds (Datatab.update (k, kind));
+  in k end;
+
+val extend_data = Datatab.map invoke_extend;
+fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
+
+end;
+
+
+
 (** build theories **)
 
 (* primitives *)
@@ -325,12 +318,12 @@
 
 local
 
-fun merge_thys pp (thy1, thy2) =
+fun merge_thys (thy1, thy2) =
   let
     val ids = merge_ids thy1 thy2;
     val history = make_history "" 0;
     val ancestry = make_ancestry [] [];
-    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
+    val data = merge_data (thy1, thy2) (data_of thy1, data_of thy2);
   in create_thy ids history ancestry data end;
 
 fun maximal_thys thys =
@@ -338,7 +331,7 @@
 
 in
 
-fun begin_thy pp name imports =
+fun begin_thy name imports =
   if name = "" then error ("Bad theory name: " ^ quote name)
   else
     let
@@ -351,7 +344,7 @@
         (case parents of
           [] => error "Missing theory imports"
         | [thy] => extend_thy thy
-        | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
+        | thy :: thys => Library.foldl merge_thys (thy, thys));
 
       val history = make_history name 0;
       val ancestry = make_ancestry parents ancestors;
@@ -498,17 +491,6 @@
 val proof_of = cases Proof_Context.init_global I;
 
 
-(* pretty printing context *)
-
-exception PRETTY of generic;
-
-val pretty_generic = Pretty o PRETTY;
-val pretty = pretty_generic o Proof;
-val pretty_global = pretty_generic o Theory;
-
-fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
-
-
 
 (** thread data **)
 
@@ -551,12 +533,12 @@
 
 (** theory data **)
 
-signature THEORY_DATA_PP_ARGS =
+signature THEORY_DATA'_ARGS =
 sig
   type T
   val empty: T
   val extend: T -> T
-  val merge: Context.pretty -> T * T -> T
+  val merge: theory * theory -> T * T -> T
 end;
 
 signature THEORY_DATA_ARGS =
@@ -575,7 +557,7 @@
   val map: (T -> T) -> theory -> theory
 end;
 
-functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
+functor Theory_Data'(Data: THEORY_DATA'_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -586,7 +568,7 @@
     (Position.thread_data ())
     (Data Data.empty)
     (fn Data x => Data (Data.extend x))
-    (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2)));
+    (fn thys => fn (Data x1, Data x2) => Data (Data.merge thys (x1, x2)));
 
 val get = Context.Theory_Data.get kind (fn Data x => x);
 val put = Context.Theory_Data.put kind Data;
@@ -595,7 +577,7 @@
 end;
 
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
-  Theory_Data_PP
+  Theory_Data'
   (
     type T = Data.T;
     val empty = Data.empty;
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/defs.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -13,6 +13,7 @@
   val item_kind_ord: item_kind * item_kind -> order
   val plain_args: typ list -> bool
   type context = Proof.context * (Name_Space.T * Name_Space.T) option
+  val global_context: theory -> context
   val space: context -> item_kind -> Name_Space.T
   val pretty_item: context -> item -> Pretty.T
   val pretty_args: Proof.context -> typ list -> Pretty.T list
@@ -55,6 +56,8 @@
 
 type context = Proof.context * (Name_Space.T * Name_Space.T) option;
 
+fun global_context thy : context = (Syntax.init_pretty_global thy, NONE);
+
 fun space (ctxt, spaces) kind =
   (case (kind, spaces) of
     (Const, SOME (const_space, _)) => const_space
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/global_theory.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -205,9 +205,9 @@
 
 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   let
-    val ctxt = Syntax.init_pretty_global thy;
+    val context as (ctxt, _) = Defs.global_context thy;
     val prop = prep ctxt (b, raw_prop);
-    val ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy;
+    val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees
       |> Thm.forall_elim_vars 0
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/more_thm.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -491,7 +491,7 @@
   in ((axm_name, thm), thy') end;
 
 fun add_def_global unchecked overloaded arg thy =
-  add_def (Syntax.init_pretty_global thy, NONE) unchecked overloaded arg thy;
+  add_def (Defs.global_context thy) unchecked overloaded arg thy;
 
 
 
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/sign.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -62,7 +62,7 @@
   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
-  val certify': bool -> Context.pretty -> bool -> Consts.T -> theory -> term -> term * typ * int
+  val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
   val certify_term: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
@@ -133,20 +133,20 @@
 
 fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
 
-structure Data = Theory_Data_PP
+structure Data = Theory_Data'
 (
   type T = sign;
   fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
 
   val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
 
-  fun merge pp (sign1, sign2) =
+  fun merge old_thys (sign1, sign2) =
     let
       val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
       val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
       val syn = Syntax.merge_syntax (syn1, syn2);
-      val tsig = Type.merge_tsig pp (tsig1, tsig2);
+      val tsig = Type.merge_tsig (Context.Theory (fst old_thys)) (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (syn, tsig, consts) end;
 );
@@ -257,7 +257,7 @@
 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.Theory thy) (tsig_of thy);
 
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
@@ -269,14 +269,14 @@
 
 local
 
-fun type_check pp tm =
+fun type_check context tm =
   let
     fun err_appl bs t T u U =
       let
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
+        val msg = Type.appl_error (Syntax.init_pretty context) t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
@@ -306,20 +306,19 @@
 
 in
 
-fun certify' prop pp do_expand consts thy tm =
+fun certify' prop context do_expand consts thy tm =
   let
     val _ = check_vars tm;
     val tm' = Term.map_types (certify_typ thy) tm;
-    val T = type_check pp tm';
+    val T = type_check context tm';
     val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
-    val tm'' = Consts.certify pp (tsig_of thy) do_expand consts tm';
+    val tm'' = Consts.certify context (tsig_of thy) do_expand consts tm';
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
-fun certify_term thy = certify' false (Context.pretty_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy =
-  #1 o certify' false (Context.pretty_global thy) false (consts_of thy) thy;
+fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
+fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
 
 end;
 
@@ -474,10 +473,10 @@
   |> add_consts [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
 fun primitive_classrel arg thy =
-  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
+  thy |> map_tsig (Type.add_classrel (Context.Theory thy) arg);
 
 fun primitive_arity arg thy =
-  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
+  thy |> map_tsig (Type.add_arity (Context.Theory thy) arg);
 
 
 (* add translation functions *)
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/sorts.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -38,15 +38,15 @@
   val minimize_sort: algebra -> sort -> sort
   val complete_sort: algebra -> sort -> sort
   val minimal_sorts: algebra -> sort list -> sort Ord_List.T
-  val add_class: Context.pretty -> class * class list -> algebra -> algebra
-  val add_classrel: Context.pretty -> class * class -> algebra -> algebra
-  val add_arities: Context.pretty -> string * (class * sort list) list -> algebra -> algebra
+  val add_class: Context.generic -> class * class list -> algebra -> algebra
+  val add_classrel: Context.generic -> class * class -> algebra -> algebra
+  val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
-  val merge_algebra: Context.pretty -> algebra * algebra -> algebra
-  val subalgebra: Context.pretty -> (class -> bool) -> (class * string -> sort list option)
+  val merge_algebra: Context.generic -> algebra * algebra -> algebra
+  val subalgebra: Context.generic -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
-  val class_error: Context.pretty -> class_error -> string
+  val class_error: Context.generic -> class_error -> string
   exception CLASS_ERROR of class_error
   val has_instance: algebra -> string -> sort -> bool
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/theory.ML
--- a/src/Pure/theory.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/theory.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -64,7 +64,7 @@
 fun make_thy (pos, id, axioms, defs, wrappers) =
   Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
 
-structure Thy = Theory_Data_PP
+structure Thy = Theory_Data'
 (
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;
@@ -73,13 +73,13 @@
   fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) =
     make_thy (Position.none, 0, empty_axioms, defs, wrappers);
 
-  fun merge pp (thy1, thy2) =
+  fun merge old_thys (thy1, thy2) =
     let
       val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = empty_axioms;
-      val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2);
+      val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
     in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
@@ -164,7 +164,7 @@
     | _ => error "Bad bootstrapping of theory Pure")
   else
     let
-      val thy = Context.begin_thy Context.pretty_global name imports;
+      val thy = Context.begin_thy name imports;
       val wrappers = begin_wrappers thy;
     in
       thy
@@ -249,7 +249,7 @@
   in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
 
 fun add_deps_global a x y thy =
-  add_deps (Syntax.init_pretty_global thy, NONE) a x y thy;
+  add_deps (Defs.global_context thy) a x y thy;
 
 fun specify_const decl thy =
   let val (t, thy') = Sign.declare_const_global decl thy;
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Pure/type.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -55,7 +55,7 @@
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
-  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
+  val arity_sorts: Context.generic -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
   val sort_of_atyp: typ -> sort
@@ -96,9 +96,9 @@
   val add_abbrev: Context.generic -> binding * string list * typ -> tsig -> tsig
   val add_nonterminal: Context.generic -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
-  val add_arity: Context.pretty -> arity -> tsig -> tsig
-  val add_classrel: Context.pretty -> class * class -> tsig -> tsig
-  val merge_tsig: Context.pretty -> tsig * tsig -> tsig
+  val add_arity: Context.generic -> arity -> tsig -> tsig
+  val add_classrel: Context.generic -> class * class -> tsig -> tsig
+  val merge_tsig: Context.generic -> tsig * tsig -> tsig
 end;
 
 structure Type: TYPE =
@@ -321,9 +321,9 @@
   | _ => error (undecl_type a));
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
-  | arity_sorts pp (TSig {classes, ...}) a S =
+  | arity_sorts context (TSig {classes, ...}) a S =
       Sorts.mg_domain (#2 classes) a S
-        handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+        handle Sorts.CLASS_ERROR err => error (Sorts.class_error context err);
 
 
 
@@ -609,7 +609,7 @@
         handle TYPE (msg, _, _) => error msg;
       val _ = Binding.check c;
       val (c', space') = space |> Name_Space.declare context true c;
-      val classes' = classes |> Sorts.add_class (Context.pretty_generic context) (c', cs');
+      val classes' = classes |> Sorts.add_class context (c', cs');
     in ((space', classes'), default, types) end);
 
 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -618,7 +618,7 @@
 
 (* arities *)
 
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity context (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   let
     val _ =
       (case lookup_type tsig t of
@@ -627,18 +627,18 @@
       | NONE => error (undecl_type t));
     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
       handle TYPE (msg, _, _) => error msg;
-    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
+    val classes' = classes |> Sorts.add_arities context ((t, map (fn c' => (c', Ss')) S'));
   in ((space, classes'), default, types) end);
 
 
 (* classrel *)
 
-fun add_classrel pp rel tsig =
+fun add_classrel context rel tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val rel' = apply2 (cert_class tsig) rel
         handle TYPE (msg, _, _) => error msg;
-      val classes' = classes |> Sorts.add_classrel pp rel';
+      val classes' = classes |> Sorts.add_classrel context rel';
     in ((space, classes'), default, types) end);
 
 
@@ -701,7 +701,7 @@
 
 (* merge type signatures *)
 
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig context (tsig1, tsig2) =
   let
     val (TSig {classes = (space1, classes1), default = default1, types = types1,
       log_types = _}) = tsig1;
@@ -709,7 +709,7 @@
       log_types = _}) = tsig2;
 
     val space' = Name_Space.merge (space1, space2);
-    val classes' = Sorts.merge_algebra pp (classes1, classes2);
+    val classes' = Sorts.merge_algebra context (classes1, classes2);
     val default' = Sorts.inter_sort classes' (default1, default2);
     val types' = Name_Space.merge_tables (types1, types2);
   in build_tsig ((space', classes'), default', types') end;
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -517,7 +517,7 @@
       |> fold (ensure_fun ctxt arities eqngr) cs
       |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
     val arities' = fold (add_arity ctxt vardeps) insts arities;
-    val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
+    val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
     fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
diff -r ddb2da7cb2e4 -r 7bd1eb4b056e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Sep 24 23:33:29 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 25 19:13:47 2015 +0200
@@ -412,7 +412,7 @@
 
 fun not_wellsorted ctxt permissive some_thm deps ty sort e =
   let
-    val err_class = Sorts.class_error (Context.pretty ctxt) e;
+    val err_class = Sorts.class_error (Context.Proof ctxt) e;
     val err_typ =
       "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
         Syntax.string_of_sort ctxt sort;