# HG changeset patch
# User wenzelm
# Date 1303131770 -7200
# Node ID 77eedb52706861112ee20631637b6f98a14f4b58
# Parent  c9bf3f8a89300d671fa199f73bd7284fb1358b8a# Parent  c65c07d9967abc51abe083539ac3b1ba7ff33e3e
merged

diff -r c9bf3f8a8930 -r 77eedb527068 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -211,7 +211,7 @@
     val tyvars = map (map (fn s =>
       (s, the (AList.lookup (op =) sorts s))) o #1) dts';
 
-    fun inter_sort thy S S' = Type.inter_sort (Sign.tsig_of thy) (S, S');
+    fun inter_sort thy S S' = Sign.inter_sort thy (S, S');
     fun augment_sort_typ thy S =
       let val S = Sign.minimize_sort thy (Sign.certify_sort thy S)
       in map_type_tfree (fn (s, S') => TFree (s,
diff -r c9bf3f8a8930 -r 77eedb527068 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -125,7 +125,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val T = domain_type (fastype_of t);
     val T' = fastype_of u;
-    val subst = Type.typ_match (Sign.tsig_of thy) (T, T') Vartab.empty
+    val subst = Sign.typ_match thy (T, T') Vartab.empty
       handle Type.TYPE_MATCH => raise TYPE ("apply_inst", [T, T'], [t, u])
   in
     map_types (Envir.norm_type subst) t $ u
diff -r c9bf3f8a8930 -r 77eedb527068 src/HOL/Tools/enriched_type.ML
--- a/src/HOL/Tools/enriched_type.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/HOL/Tools/enriched_type.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -218,10 +218,11 @@
     val qualify = Binding.qualify true prfx o Binding.name;
     fun mapper_declaration comp_thm id_thm phi context =
       let
-        val typ_instance = Type.typ_instance (Proof_Context.tsig_of (Context.proof_of context));
+        val typ_instance = Sign.typ_instance (Context.theory_of context);
         val mapper' = Morphism.term phi mapper;
         val T_T' = pairself fastype_of (mapper, mapper');
-      in if typ_instance T_T' andalso typ_instance (swap T_T')
+      in
+        if typ_instance T_T' andalso typ_instance (swap T_T')
         then (Data.map o Symtab.cons_list) (tyco,
           { mapper = mapper', variances = variances,
             comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/General/pretty.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -64,18 +64,6 @@
   val writeln: T -> unit
   val to_ML: T -> ML_Pretty.pretty
   val from_ML: ML_Pretty.pretty -> T
-  type pp
-  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
-  val term: pp -> term -> T
-  val typ: pp -> typ -> T
-  val sort: pp -> sort -> T
-  val classrel: pp -> class list -> T
-  val arity: pp -> arity -> T
-  val string_of_term: pp -> term -> string
-  val string_of_typ: pp -> typ -> string
-  val string_of_sort: pp -> sort -> string
-  val string_of_classrel: pp -> class list -> string
-  val string_of_arity: pp -> arity -> string
 end;
 
 structure Pretty: PRETTY =
@@ -332,27 +320,4 @@
 
 end;
 
-
-
-(** abstract pretty printing context **)
-
-datatype pp =
-  PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
-
-val pp = PP;
-
-fun pp_fun f (PP x) = f x;
-
-val term     = pp_fun #1;
-val typ      = pp_fun #2;
-val sort     = pp_fun #3;
-val classrel = pp_fun #4;
-val arity    = pp_fun #5;
-
-val string_of_term     = string_of oo term;
-val string_of_typ      = string_of oo typ;
-val string_of_sort     = string_of oo sort;
-val string_of_classrel = string_of oo classrel;
-val string_of_arity    = string_of oo arity;
-
 end;
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/class.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -450,15 +450,16 @@
             (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
   end;
 
-fun resort_terms pp algebra consts constraints ts =
+fun resort_terms ctxt algebra consts constraints ts =
   let
-    fun matchings (Const (c_ty as (c, _))) = (case constraints c
-         of NONE => I
-          | SOME sorts => fold2 (curry (Sorts.meet_sort algebra))
-              (Consts.typargs consts c_ty) sorts)
-      | matchings _ = I
+    fun matchings (Const (c_ty as (c, _))) =
+          (case constraints c of
+            NONE => I
+          | SOME sorts =>
+              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 pp e);
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error 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 NONE else SOME ((map o map_types) inst ts) end;
@@ -529,19 +530,20 @@
     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 (Syntax.pp_global thy)
+      |> fold (fn tyco => Sorts.add_arities (Proof_Context.init_global thy)
             (tyco, map (fn class => (class, map snd vs)) sort)) tycos;
     val consts = Sign.consts_of thy;
     val improve_constraints = AList.lookup (op =)
       (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
-    fun resort_check ts ctxt = case resort_terms (Syntax.pp ctxt) algebra consts improve_constraints ts
-     of NONE => NONE
-      | SOME ts' => SOME (ts', ctxt);
+    fun resort_check ts ctxt =
+      (case resort_terms ctxt algebra consts improve_constraints ts of
+        NONE => NONE
+      | SOME ts' => SOME (ts', ctxt));
     val lookup_inst_param = AxClass.lookup_inst_param consts params;
-    val typ_instance = Type.typ_instance (Sign.tsig_of thy);
-    fun improve (c, ty) = case lookup_inst_param (c, ty)
-     of SOME (_, ty') => if typ_instance (ty', ty) then SOME (ty, ty') else NONE
-      | NONE => NONE;
+    fun improve (c, ty) =
+      (case lookup_inst_param (c, ty) of
+        SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
+      | NONE => NONE);
   in
     thy
     |> Theory.checkpoint
@@ -559,7 +561,8 @@
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
         abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+            Generic_Target.theory_abbrev prmode ((b, mx), t)),
         declaration = K Generic_Target.theory_declaration,
         syntax_declaration = K Generic_Target.theory_declaration,
         pretty = pretty,
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -63,20 +63,25 @@
 
 fun improve_term_check ts ctxt =
   let
+    val thy = Proof_Context.theory_of ctxt;
+
     val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } =
       ImprovableSyntax.get ctxt;
-    val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt;
     val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
     val passed_or_abbrev = passed orelse is_abbrev;
-    fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
-         of SOME ty_ty' => Type.typ_match tsig ty_ty'
+    fun accumulate_improvements (Const (c, ty)) =
+          (case improve (c, ty) of
+            SOME ty_ty' => Sign.typ_match thy ty_ty'
           | _ => I)
       | accumulate_improvements _ = I;
     val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
     val ts' = (map o map_types) (Envir.subst_type improvements) ts;
-    fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty)
-         of SOME (ty', t') =>
-              if Type.typ_instance tsig (ty, ty')
+    fun apply_subst t =
+      Envir.expand_term
+        (fn Const (c, ty) =>
+          (case subst (c, ty) of
+            SOME (ty', t') =>
+              if Sign.typ_instance thy (ty, ty')
               then SOME (ty', apply_subst t') else NONE
           | NONE => NONE)
         | _ => NONE) t;
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -302,7 +302,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 (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
+      else (Type.merge_tsig ctxt (local_tsig, thy_tsig), thy_tsig)
     end) |>
   map_consts (fn consts as (local_consts, global_consts) =>
     let val thy_consts = Sign.consts_of thy in
@@ -376,7 +376,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 (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
+  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
 
 in
 
@@ -546,7 +546,7 @@
 
 local
 
-fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
+fun certify_consts ctxt = Consts.certify (Context.pretty ctxt) (tsig_of ctxt)
   (not (abbrev_mode ctxt)) (consts_of ctxt);
 
 fun expand_binds ctxt =
@@ -666,9 +666,9 @@
 fun gen_cert prop ctxt t =
   t
   |> expand_abbrevs ctxt
-  |> (fn t' => #1 (Sign.certify' prop (Syntax.pp ctxt) false (consts_of ctxt) (theory_of ctxt) t')
-    handle TYPE (msg, _, _) => error msg
-      | TERM (msg, _) => error msg);
+  |> (fn t' =>
+      #1 (Sign.certify' prop (Context.pretty ctxt) false (consts_of ctxt) (theory_of ctxt) t')
+        handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
 
 in
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -53,6 +53,7 @@
 use "General/xml.ML";
 use "General/xml_data.ML";
 use "General/yxml.ML";
+use "General/pretty.ML";
 
 use "General/sha1.ML";
 if String.isPrefix "polyml" ml_system
@@ -103,24 +104,15 @@
 
 use "name.ML";
 use "term.ML";
-use "term_ord.ML";
-use "term_subst.ML";
-use "old_term.ML";
-use "General/pretty.ML";
 use "context.ML";
 use "config.ML";
 use "context_position.ML";
-use "General/name_space.ML";
-use "sorts.ML";
-use "type.ML";
-use "logic.ML";
 
 
 (* inner syntax *)
 
 use "Syntax/term_position.ML";
 use "Syntax/lexicon.ML";
-use "Syntax/simple_syntax.ML";
 use "Syntax/ast.ML";
 use "Syntax/syntax_ext.ML";
 use "Syntax/parser.ML";
@@ -132,6 +124,14 @@
 
 (* core of tactical proof system *)
 
+use "term_ord.ML";
+use "term_subst.ML";
+use "old_term.ML";
+use "General/name_space.ML";
+use "sorts.ML";
+use "type.ML";
+use "logic.ML";
+use "Syntax/simple_syntax.ML";
 use "net.ML";
 use "item_net.ML";
 use "envir.ML";
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -36,12 +36,12 @@
   val pretty_term_ast: bool -> Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> string -> Pretty.T option) ->
-    (string -> Markup.T list * xstring) ->
+    (string -> Markup.T list * string) ->
     Ast.ast -> Pretty.T list
   val pretty_typ_ast: Proof.context -> prtabs ->
     (string -> Proof.context -> Ast.ast list -> Ast.ast) ->
     (string -> string -> Pretty.T option) ->
-    (string -> Markup.T list * xstring) -> Ast.ast -> Pretty.T list
+    (string -> Markup.T list * string) -> Ast.ast -> Pretty.T list
 end;
 
 structure Printer: PRINTER =
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -10,6 +10,8 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
+  type operations
+  val install_operations: operations -> unit
   val root: string Config.T
   val positions_raw: Config.raw
   val positions: bool Config.T
@@ -28,14 +30,6 @@
   val unparse_arity: Proof.context -> arity -> Pretty.T
   val unparse_typ: Proof.context -> typ -> Pretty.T
   val unparse_term: Proof.context -> term -> Pretty.T
-  val install_operations:
-   {parse_sort: Proof.context -> string -> sort,
-    parse_typ: Proof.context -> string -> typ,
-    parse_term: Proof.context -> string -> term,
-    parse_prop: Proof.context -> string -> term,
-    unparse_sort: Proof.context -> sort -> Pretty.T,
-    unparse_typ: Proof.context -> typ -> Pretty.T,
-    unparse_term: Proof.context -> term -> Pretty.T} -> unit
   val print_checks: Proof.context -> unit
   val add_typ_check: int -> string ->
     (typ list -> Proof.context -> (typ list * Proof.context) option) ->
@@ -49,6 +43,10 @@
   val add_term_uncheck: int -> string ->
     (term list -> Proof.context -> (term list * Proof.context) option) ->
     Context.generic -> Context.generic
+  val typ_check: Proof.context -> typ list -> typ list
+  val term_check: Proof.context -> term list -> term list
+  val typ_uncheck: Proof.context -> typ list -> typ list
+  val term_uncheck: Proof.context -> term list -> term list
   val check_sort: Proof.context -> sort -> sort
   val check_typ: Proof.context -> typ -> typ
   val check_term: Proof.context -> term -> term
@@ -84,14 +82,13 @@
   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 pretty_term_global: theory -> term -> Pretty.T
   val pretty_typ_global: theory -> typ -> Pretty.T
   val pretty_sort_global: theory -> sort -> Pretty.T
   val string_of_term_global: theory -> term -> string
   val string_of_typ_global: theory -> typ -> string
   val string_of_sort_global: theory -> sort -> string
-  val pp: Proof.context -> Pretty.pp
-  val pp_global: theory -> Pretty.pp
   type syntax
   val eq_syntax: syntax * syntax -> bool
   val lookup_const: syntax -> string -> string option
@@ -151,6 +148,31 @@
 
 (** inner syntax operations **)
 
+(* back-patched operations *)
+
+type operations =
+ {parse_sort: Proof.context -> string -> sort,
+  parse_typ: Proof.context -> string -> typ,
+  parse_term: Proof.context -> string -> term,
+  parse_prop: Proof.context -> string -> term,
+  unparse_sort: Proof.context -> sort -> Pretty.T,
+  unparse_typ: Proof.context -> typ -> Pretty.T,
+  unparse_term: Proof.context -> term -> Pretty.T,
+  check_typs: Proof.context -> typ list -> typ list,
+  check_terms: Proof.context -> term list -> term list,
+  check_props: Proof.context -> term list -> term list,
+  uncheck_typs: Proof.context -> typ list -> typ list,
+  uncheck_terms: Proof.context -> term list -> term list};
+
+val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
+fun install_operations ops = Single_Assignment.assign operations ops;
+
+fun operation which ctxt x =
+  (case Single_Assignment.peek operations of
+    NONE => raise Fail "Inner syntax operations not installed"
+  | SOME ops => which ops ctxt x);
+
+
 (* configuration options *)
 
 val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
@@ -191,26 +213,6 @@
     val _ = Context_Position.report ctxt pos markup;
   in (syms, pos) end;
 
-local
-
-type operations =
- {parse_sort: Proof.context -> string -> sort,
-  parse_typ: Proof.context -> string -> typ,
-  parse_term: Proof.context -> string -> term,
-  parse_prop: Proof.context -> string -> term,
-  unparse_sort: Proof.context -> sort -> Pretty.T,
-  unparse_typ: Proof.context -> typ -> Pretty.T,
-  unparse_term: Proof.context -> term -> Pretty.T};
-
-val operations: operations Single_Assignment.var = Single_Assignment.var "Syntax.operations";
-
-fun operation which ctxt x =
-  (case Single_Assignment.peek operations of
-    NONE => raise Fail "Inner syntax operations not installed"
-  | SOME ops => which ops ctxt x);
-
-in
-
 val parse_sort = operation #parse_sort;
 val parse_typ = operation #parse_typ;
 val parse_term = operation #parse_term;
@@ -219,10 +221,6 @@
 val unparse_typ = operation #unparse_typ;
 val unparse_term = operation #unparse_term;
 
-fun install_operations ops = Single_Assignment.assign operations ops;
-
-end;
-
 
 (* context-sensitive (un)checking *)
 
@@ -290,17 +288,22 @@
 fun add_typ_uncheck stage = gen_add apfst (stage, true);
 fun add_term_uncheck stage = gen_add apsnd (stage, true);
 
-val check_typs = gen_check fst false;
-val check_terms = gen_check snd false;
-fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+val typ_check = gen_check fst false;
+val term_check = gen_check snd false;
+val typ_uncheck = gen_check fst true;
+val term_uncheck = gen_check snd true;
+
+val check_typs = operation #check_typs;
+val check_terms = operation #check_terms;
+val check_props = operation #check_props;
 
 val check_typ = singleton o check_typs;
 val check_term = singleton o check_terms;
 val check_prop = singleton o check_props;
 val check_sort = map_sort o check_typ;
 
-val uncheck_typs = gen_check fst true;
-val uncheck_terms = gen_check snd true;
+val uncheck_typs = operation #uncheck_typs;
+val uncheck_terms = operation #uncheck_terms;
 val uncheck_sort = map_sort o singleton o uncheck_typs;
 
 end;
@@ -371,6 +374,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 pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;
@@ -381,23 +385,6 @@
 val string_of_sort_global = string_of_sort o init_pretty_global;
 
 
-(* pp operations -- deferred evaluation *)
-
-fun pp ctxt = Pretty.pp
- (fn x => pretty_term ctxt x,
-  fn x => pretty_typ ctxt x,
-  fn x => pretty_sort ctxt x,
-  fn x => pretty_classrel ctxt x,
-  fn x => pretty_arity ctxt x);
-
-fun pp_global thy = Pretty.pp
- (fn x => pretty_term_global thy x,
-  fn x => pretty_typ_global thy x,
-  fn x => pretty_sort_global thy x,
-  fn x => pretty_classrel (init_pretty_global thy) x,
-  fn x => pretty_arity (init_pretty_global thy) x);
-
-
 
 (** tables of translation functions **)
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -702,6 +702,17 @@
 
 
 
+(** check/uncheck **)
+
+val check_typs = Syntax.typ_check;
+val check_terms = Syntax.term_check;
+fun check_props ctxt = map (Type.constraint propT) #> check_terms ctxt;
+
+val uncheck_typs = Syntax.typ_uncheck;
+val uncheck_terms = Syntax.term_uncheck;
+
+
+
 (** install operations **)
 
 val _ = Syntax.install_operations
@@ -711,6 +722,11 @@
    parse_prop = parse_term true,
    unparse_sort = unparse_sort,
    unparse_typ = unparse_typ,
-   unparse_term = unparse_term};
+   unparse_term = unparse_term,
+   check_typs = check_typs,
+   check_terms = check_terms,
+   check_props = check_props,
+   uncheck_typs = uncheck_typs,
+   uncheck_terms = uncheck_terms};
 
 end;
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/axclass.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -59,12 +59,12 @@
 
 type param = string * class;
 
-fun add_param pp ((x, c): param) params =
+fun add_param ctxt ((x, c): param) params =
   (case AList.lookup (op =) params x of
     NONE => (x, c) :: params
-  | SOME c' => error ("Duplicate class parameter " ^ quote x ^
-      " for " ^ Pretty.string_of_sort pp [c] ^
-      (if c = c' then "" else " and " ^ Pretty.string_of_sort pp [c'])));
+  | SOME c' =>
+      error ("Duplicate class parameter " ^ quote x ^ " for " ^ Syntax.string_of_sort ctxt [c] ^
+        (if c = c' then "" else " and " ^ Syntax.string_of_sort ctxt [c'])));
 
 
 (* setup data *)
@@ -104,10 +104,14 @@
         proven_arities = proven_arities2, inst_params = inst_params2,
         diff_classrels = diff_classrels2}) =
     let
+      val ctxt = Syntax.init_pretty pp;
+
       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 pp p) params2 params1;
+        else
+          fold_rev (fn p => if member (op =) params1 p then I else add_param ctxt p)
+            params2 params1;
 
       (*transitive closure of classrels and arity completion is done in Theory.at_begin hook*)
       val proven_classrels' = Symreltab.join (K #1) (proven_classrels1, proven_classrels2);
@@ -590,7 +594,7 @@
       |> #2
       |> Sign.restore_naming facts_thy
       |> map_axclasses (Symtab.update (class, axclass))
-      |> map_params (fold (fn (x, _) => add_param (Syntax.pp ctxt) (x, class)) params);
+      |> map_params (fold (fn (x, _) => add_param ctxt (x, class)) params);
 
   in (class, result_thy) end;
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/consts.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -26,7 +26,7 @@
   val intern_syntax: T -> xstring -> string
   val extern_syntax: Proof.context -> T -> string -> xstring
   val read_const: T -> string -> term
-  val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
+  val certify: Context.pretty -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
   val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
@@ -156,7 +156,8 @@
 fun certify pp tsig do_expand consts =
   let
     fun err msg (c, T) =
-      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []);
+      raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
+        Syntax.string_of_typ (Syntax.init_pretty pp) T, [], []);
     val certT = Type.cert_typ tsig;
     fun cert tm =
       let
@@ -269,7 +270,7 @@
 
 fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   let
-    val pp = Syntax.pp ctxt;
+    val pp = Context.pretty ctxt;
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = Print_Mode.internal;
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/context.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -28,6 +28,7 @@
 sig
   include BASIC_CONTEXT
   (*theory context*)
+  type pretty
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_name: theory -> string
@@ -52,7 +53,7 @@
   val copy_thy: theory -> theory
   val checkpoint_thy: theory -> theory
   val finish_thy: theory -> theory
-  val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
+  val begin_thy: (theory -> pretty) -> string -> theory list -> theory
   (*proof context*)
   val raw_transfer: theory -> Proof.context -> Proof.context
   (*generic context*)
@@ -71,6 +72,10 @@
   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_context: (theory -> Proof.context) -> pretty -> Proof.context
   (*thread data*)
   val thread_data: unit -> generic option
   val the_thread_data: unit -> generic
@@ -86,7 +91,7 @@
   structure Theory_Data:
   sig
     val declare: Object.T -> (Object.T -> Object.T) ->
-      (Pretty.pp -> Object.T * Object.T -> Object.T) -> serial
+      (pretty -> Object.T * Object.T -> Object.T) -> serial
     val get: serial -> (Object.T -> 'a) -> theory -> 'a
     val put: serial -> ('a -> Object.T) -> 'a -> theory -> theory
   end
@@ -110,12 +115,14 @@
 (*private copy avoids potential conflict of table exceptions*)
 structure Datatab = Table(type key = int val ord = int_ord);
 
+datatype pretty = Pretty of Object.T;
+
 local
 
 type kind =
  {empty: Object.T,
   extend: Object.T -> Object.T,
-  merge: Pretty.pp -> Object.T * Object.T -> Object.T};
+  merge: pretty -> Object.T * Object.T -> Object.T};
 
 val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
 
@@ -546,6 +553,16 @@
 val proof_of = cases Proof_Context.init_global I;
 
 
+(* pretty printing context *)
+
+exception PRETTY of generic;
+
+val pretty = Pretty o PRETTY o Proof;
+val pretty_global = Pretty o PRETTY o Theory;
+
+fun pretty_context init (Pretty (PRETTY context)) = cases init I context;
+
+
 
 (** thread data **)
 
@@ -593,7 +610,7 @@
   type T
   val empty: T
   val extend: T -> T
-  val merge: Pretty.pp -> T * T -> T
+  val merge: Context.pretty -> T * T -> T
 end;
 
 signature THEORY_DATA_ARGS =
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/defs.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -7,7 +7,7 @@
 
 signature DEFS =
 sig
-  val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
+  val pretty_const: Proof.context -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
   type spec =
@@ -18,8 +18,8 @@
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
-  val merge: Pretty.pp -> T * T -> T
-  val define: Pretty.pp -> bool -> string option -> string ->
+  val merge: Proof.context -> T * T -> T
+  val define: Proof.context -> bool -> string option -> string ->
     string * typ list -> (string * typ list) list -> T -> T
 end
 
@@ -30,11 +30,11 @@
 
 type args = typ list;
 
-fun pretty_const pp (c, args) =
+fun pretty_const ctxt (c, args) =
   let
     val prt_args =
       if null args then []
-      else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT_global) args)];
+      else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
   in Pretty.block (Pretty.str c :: prt_args) end;
 
 fun plain_args args =
@@ -118,27 +118,27 @@
 local
 
 val prt = Pretty.string_of oo pretty_const;
-fun err pp (c, args) (d, Us) s1 s2 =
-  error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " -> " ^ prt pp (d, Us) ^ s2);
+fun err ctxt (c, args) (d, Us) s1 s2 =
+  error (s1 ^ " dependency of constant " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
 
 fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts
   | contained _ _ = false;
 
-fun acyclic pp (c, args) (d, Us) =
+fun acyclic ctxt (c, args) (d, Us) =
   c <> d orelse
   exists (fn U => exists (contained U) args) Us orelse
   is_none (match_args (args, Us)) orelse
-  err pp (c, args) (d, Us) "Circular" "";
+  err ctxt (c, args) (d, Us) "Circular" "";
 
-fun wellformed pp defs (c, args) (d, Us) =
+fun wellformed ctxt defs (c, args) (d, Us) =
   forall is_TVar Us orelse
   (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
     SOME (Ts, description) =>
-      err pp (c, args) (d, Us) "Malformed"
-        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote description ^ ")")
+      err ctxt (c, args) (d, Us) "Malformed"
+        ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
   | NONE => true);
 
-fun reduction pp defs const deps =
+fun reduction ctxt defs const deps =
   let
     fun reduct Us (Ts, rhs) =
       (case match_args (Ts, Us) of
@@ -151,17 +151,17 @@
       if forall (is_none o #1) reds then NONE
       else SOME (fold_rev
         (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
-    val _ = forall (acyclic pp const) (the_default deps deps');
+    val _ = forall (acyclic ctxt const) (the_default deps deps');
   in deps' end;
 
 in
 
-fun normalize pp =
+fun normalize ctxt =
   let
     fun norm_update (c, {reducts, ...}: def) (changed, defs) =
       let
         val reducts' = reducts |> map (fn (args, deps) =>
-          (args, perhaps (reduction pp defs (c, args)) deps));
+          (args, perhaps (reduction ctxt defs (c, args)) deps));
       in
         if reducts = reducts' then (changed, defs)
         else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
@@ -171,38 +171,38 @@
         (true, defs') => norm_all defs'
       | (false, _) => defs);
     fun check defs (c, {reducts, ...}: def) =
-      reducts |> forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps);
+      reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
   in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end;
 
-fun dependencies pp (c, args) restr deps =
+fun dependencies ctxt (c, args) restr deps =
   map_def c (fn (specs, restricts, reducts) =>
     let
       val restricts' = Library.merge (op =) (restricts, restr);
       val reducts' = insert (op =) (args, deps) reducts;
     in (specs, restricts', reducts') end)
-  #> normalize pp;
+  #> normalize ctxt;
 
 end;
 
 
 (* merge *)
 
-fun merge pp (Defs defs1, Defs defs2) =
+fun merge ctxt (Defs defs1, Defs defs2) =
   let
     fun add_deps (c, args) restr deps defs =
       if AList.defined (op =) (reducts_of defs c) args then defs
-      else dependencies pp (c, args) restr deps defs;
+      else dependencies ctxt (c, args) restr deps defs;
     fun add_def (c, {restricts, reducts, ...}: def) =
       fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   in
     Defs (Symtab.join join_specs (defs1, defs2)
-      |> normalize pp |> Symtab.fold add_def defs2)
+      |> normalize ctxt |> Symtab.fold add_def defs2)
   end;
 
 
 (* define *)
 
-fun define pp unchecked def description (c, args) deps (Defs defs) =
+fun define ctxt unchecked def description (c, args) deps (Defs defs) =
   let
     val restr =
       if plain_args args orelse
@@ -211,6 +211,6 @@
     val spec =
       (serial (), {def = def, description = description, lhs = args, rhs = deps});
     val defs' = defs |> update_specs c spec;
-  in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
+  in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
 
 end;
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/display.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -143,7 +143,7 @@
     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
     val prt_term_no_vars = prt_term o Logic.unvarify_global;
     fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
-    val prt_const' = Defs.pretty_const (Syntax.pp ctxt);
+    val prt_const' = Defs.pretty_const ctxt;
 
     fun pretty_classrel (c, []) = prt_cls c
       | pretty_classrel (c, cs) = Pretty.block
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/sign.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -61,7 +61,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 -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
+  val certify': bool -> Context.pretty -> 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
@@ -144,12 +144,13 @@
 
   fun merge pp (sign1, sign2) =
     let
+      val ctxt = Syntax.init_pretty pp;
       val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
       val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
 
       val naming = Name_Space.default_naming;
       val syn = Syntax.merge_syntaxes syn1 syn2;
-      val tsig = Type.merge_tsig pp (tsig1, tsig2);
+      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
       val consts = Consts.merge (consts1, consts2);
     in make_sign (naming, syn, tsig, consts) end;
 );
@@ -243,11 +244,11 @@
 (* certify wrt. type signature *)
 
 val arity_number = Type.arity_number o tsig_of;
-fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
+fun arity_sorts thy = Type.arity_sorts (Context.pretty_global thy) (tsig_of thy);
 
-val certify_class         = Type.cert_class o tsig_of;
-val certify_sort          = Type.cert_sort o tsig_of;
-val certify_typ           = Type.cert_typ o tsig_of;
+val certify_class = Type.cert_class o tsig_of;
+val certify_sort = Type.cert_sort o tsig_of;
+val certify_typ = Type.cert_typ o tsig_of;
 fun certify_typ_mode mode = Type.cert_typ_mode mode o tsig_of;
 
 
@@ -262,7 +263,7 @@
         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 pp t' T u' U;
+        val msg = Type.appl_error (Syntax.init_pretty pp) t' T u' U;
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T
@@ -301,10 +302,11 @@
     val tm'' = Consts.certify pp (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 (Syntax.pp_global thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
+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;
 val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
+fun cert_prop thy = #1 o certify' true (Context.pretty_global thy) true (consts_of thy) thy;
 
 end;
 
@@ -454,15 +456,19 @@
 (* primitive classes and arities *)
 
 fun primitive_class (bclass, classes) thy =
-  thy |> map_sign (fn (naming, syn, tsig, consts) =>
+  thy
+  |> map_sign (fn (naming, syn, tsig, consts) =>
     let
       val ctxt = Syntax.init_pretty_global thy;
-      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
+      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
     in (naming, syn, tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
-fun primitive_classrel arg thy = thy |> map_tsig (Type.add_classrel (Syntax.pp_global thy) arg);
-fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Syntax.pp_global thy) arg);
+fun primitive_classrel arg thy =
+  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
+
+fun primitive_arity arg thy =
+  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
 
 
 (* add translation functions *)
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/sorts.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -40,15 +40,15 @@
   val minimal_sorts: algebra -> sort list -> sort Ord_List.T
   val certify_class: algebra -> class -> class    (*exception TYPE*)
   val certify_sort: algebra -> sort -> sort       (*exception TYPE*)
-  val add_class: Pretty.pp -> class * class list -> algebra -> algebra
-  val add_classrel: Pretty.pp -> class * class -> algebra -> algebra
-  val add_arities: Pretty.pp -> string * (class * sort list) list -> algebra -> algebra
+  val add_class: Proof.context -> class * class list -> algebra -> algebra
+  val add_classrel: Proof.context -> class * class -> algebra -> algebra
+  val add_arities: Proof.context -> string * (class * sort list) list -> algebra -> algebra
   val empty_algebra: algebra
-  val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
-  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
+  val merge_algebra: Proof.context -> algebra * algebra -> algebra
+  val subalgebra: Proof.context -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
-  val class_error: Pretty.pp -> class_error -> string
+  val class_error: Proof.context -> class_error -> string
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
   val meet_sort: algebra -> typ * sort
@@ -198,16 +198,16 @@
 
 fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
 
-fun err_cyclic_classes pp css =
+fun err_cyclic_classes ctxt css =
   error (cat_lines (map (fn cs =>
-    "Cycle in class relation: " ^ Pretty.string_of_classrel pp cs) css));
+    "Cycle in class relation: " ^ Syntax.string_of_classrel ctxt cs) css));
 
-fun add_class pp (c, cs) = map_classes (fn classes =>
+fun add_class ctxt (c, cs) = map_classes (fn classes =>
   let
     val classes' = classes |> Graph.new_node (c, serial ())
       handle Graph.DUP dup => err_dup_class dup;
     val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs)
-      handle Graph.CYCLES css => err_cyclic_classes pp css;
+      handle Graph.CYCLES css => err_cyclic_classes ctxt css;
   in classes'' end);
 
 
@@ -216,15 +216,14 @@
 local
 
 fun for_classes _ NONE = ""
-  | for_classes pp (SOME (c1, c2)) =
-      " for classes " ^ Pretty.string_of_classrel pp [c1, c2];
+  | for_classes ctxt (SOME (c1, c2)) = " for classes " ^ Syntax.string_of_classrel ctxt [c1, c2];
 
-fun err_conflict pp t cc (c, Ss) (c', Ss') =
-  error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n  " ^
-    Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n  " ^
-    Pretty.string_of_arity pp (t, Ss', [c']));
+fun err_conflict ctxt t cc (c, Ss) (c', Ss') =
+  error ("Conflict of type arities" ^ for_classes ctxt cc ^ ":\n  " ^
+    Syntax.string_of_arity ctxt (t, Ss, [c]) ^ " and\n  " ^
+    Syntax.string_of_arity ctxt (t, Ss', [c']));
 
-fun coregular pp algebra t (c, Ss) ars =
+fun coregular ctxt algebra t (c, Ss) ars =
   let
     fun conflict (c', Ss') =
       if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -234,62 +233,62 @@
       else NONE;
   in
     (case get_first conflict ars of
-      SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
+      SOME ((c1, c2), (c', Ss')) => err_conflict ctxt t (SOME (c1, c2)) (c, Ss) (c', Ss')
     | NONE => (c, Ss) :: ars)
   end;
 
 fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
 
-fun insert pp algebra t (c, Ss) ars =
+fun insert ctxt algebra t (c, Ss) ars =
   (case AList.lookup (op =) ars c of
-    NONE => coregular pp algebra t (c, Ss) ars
+    NONE => coregular ctxt algebra t (c, Ss) ars
   | SOME Ss' =>
       if sorts_le algebra (Ss, Ss') then ars
       else if sorts_le algebra (Ss', Ss)
-      then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
-      else err_conflict pp t NONE (c, Ss) (c, Ss'));
+      then coregular ctxt algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+      else err_conflict ctxt t NONE (c, Ss) (c, Ss'));
 
 in
 
-fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+fun insert_ars ctxt algebra t = fold_rev (insert ctxt algebra t);
 
-fun insert_complete_ars pp algebra (t, ars) arities =
+fun insert_complete_ars ctxt algebra (t, ars) arities =
   let val ars' =
     Symtab.lookup_list arities t
-    |> fold_rev (insert_ars pp algebra t) (map (complete algebra) ars);
+    |> fold_rev (insert_ars ctxt algebra t) (map (complete algebra) ars);
   in Symtab.update (t, ars') arities end;
 
-fun add_arities pp arg algebra =
-  algebra |> map_arities (insert_complete_ars pp algebra arg);
+fun add_arities ctxt arg algebra =
+  algebra |> map_arities (insert_complete_ars ctxt algebra arg);
 
-fun add_arities_table pp algebra =
-  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
+fun add_arities_table ctxt algebra =
+  Symtab.fold (fn (t, ars) => insert_complete_ars ctxt algebra (t, ars));
 
 end;
 
 
 (* classrel *)
 
-fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities ctxt algebra = algebra |> map_arities (fn arities =>
   Symtab.empty
-  |> add_arities_table pp algebra arities);
+  |> add_arities_table ctxt algebra arities);
 
-fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
+fun add_classrel ctxt rel = rebuild_arities ctxt o map_classes (fn classes =>
   classes |> Graph.add_edge_trans_acyclic rel
-    handle Graph.CYCLES css => err_cyclic_classes pp css);
+    handle Graph.CYCLES css => err_cyclic_classes ctxt css);
 
 
 (* empty and merge *)
 
 val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
 
-fun merge_algebra pp
+fun merge_algebra ctxt
    (Algebra {classes = classes1, arities = arities1},
     Algebra {classes = classes2, arities = arities2}) =
   let
     val classes' = Graph.merge_trans_acyclic (op =) (classes1, classes2)
       handle Graph.DUP c => err_dup_class c
-        | Graph.CYCLES css => err_cyclic_classes pp css;
+        | Graph.CYCLES css => err_cyclic_classes ctxt css;
     val algebra0 = make_algebra (classes', Symtab.empty);
     val arities' =
       (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -297,20 +296,20 @@
       | (true, false) =>  (*no completion*)
           (arities1, arities2) |> Symtab.join (fn t => fn (ars1, ars2) =>
             if pointer_eq (ars1, ars2) then raise Symtab.SAME
-            else insert_ars pp algebra0 t ars2 ars1)
+            else insert_ars ctxt algebra0 t ars2 ars1)
       | (false, true) =>  (*unary completion*)
           Symtab.empty
-          |> add_arities_table pp algebra0 arities1
+          |> add_arities_table ctxt algebra0 arities1
       | (false, false) => (*binary completion*)
           Symtab.empty
-          |> add_arities_table pp algebra0 arities1
-          |> add_arities_table pp algebra0 arities2);
+          |> add_arities_table ctxt algebra0 arities1
+          |> add_arities_table ctxt algebra0 arities2);
   in make_algebra (classes', arities') end;
 
 
 (* algebra projections *)  (* FIXME potentially violates abstract type integrity *)
 
-fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
+fun subalgebra ctxt P sargs (algebra as Algebra {classes, arities}) =
   let
     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
     fun restrict_arity t (c, Ss) =
@@ -322,7 +321,7 @@
       else NONE;
     val classes' = classes |> Graph.subgraph P;
     val arities' = arities |> Symtab.map (map_filter o restrict_arity);
-  in (restrict_sort, rebuild_arities pp (make_algebra (classes', arities'))) end;
+  in (restrict_sort, rebuild_arities ctxt (make_algebra (classes', arities'))) end;
 
 
 
@@ -335,13 +334,13 @@
   No_Arity of string * class |
   No_Subsort of sort * sort;
 
-fun class_error pp (No_Classrel (c1, c2)) =
-      "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
-  | class_error pp (No_Arity (a, c)) =
-      "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
-  | class_error pp (No_Subsort (S1, S2)) =
-     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
-       ^ " < " ^ Pretty.string_of_sort pp S2;
+fun class_error ctxt (No_Classrel (c1, c2)) =
+      "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
+  | class_error ctxt (No_Arity (a, c)) =
+      "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
+  | class_error ctxt (No_Subsort (S1, S2)) =
+      "Cannot derive subsort relation " ^
+        Syntax.string_of_sort ctxt S1 ^ " < " ^ Syntax.string_of_sort ctxt S2;
 
 exception CLASS_ERROR of class_error;
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/theory.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -95,11 +95,12 @@
 
   fun merge pp (thy1, thy2) =
     let
+      val ctxt = Syntax.init_pretty pp;
       val Thy {axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
       val Thy {axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
 
       val axioms' = empty_axioms;
-      val defs' = Defs.merge pp (defs1, defs2);
+      val defs' = Defs.merge ctxt (defs1, defs2);
       val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
       val ens' = Library.merge (eq_snd op =) (ens1, ens2);
     in make_thy (axioms', defs', (bgs', ens')) end;
@@ -137,7 +138,7 @@
 
 fun begin_theory name imports =
   let
-    val thy = Context.begin_thy Syntax.pp_global name imports;
+    val thy = Context.begin_thy Context.pretty_global name imports;
     val wrappers = begin_wrappers thy;
   in
     thy
@@ -196,7 +197,7 @@
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
         "\nThe error(s) above occurred in " ^ quote description);
-  in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
+  in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
 
 fun add_deps ctxt a raw_lhs raw_rhs thy =
   let
@@ -239,9 +240,8 @@
 
 local
 
-fun check_def ctxt unchecked overloaded (b, tm) defs =
+fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
@@ -258,7 +258,7 @@
 fun add_def ctxt unchecked overloaded raw_axm thy =
   let val axm = cert_axm ctxt raw_axm in
     thy
-    |> map_defs (check_def ctxt unchecked overloaded axm)
+    |> map_defs (check_def ctxt thy unchecked overloaded axm)
     |> add_axiom ctxt axm
   end;
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/type.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -11,7 +11,7 @@
   val mark_polymorphic: typ -> typ
   val constraint: typ -> term -> term
   val strip_constraints: term -> term
-  val appl_error: Pretty.pp -> term -> typ -> term -> typ -> string
+  val appl_error: Proof.context -> term -> typ -> term -> typ -> string
   (*type signatures and certified types*)
   datatype decl =
     LogicalType of int |
@@ -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: Pretty.pp -> tsig -> string -> sort -> sort list
+  val arity_sorts: Context.pretty -> tsig -> string -> sort -> sort list
 
   (*special treatment of type vars*)
   val sort_of_atyp: typ -> sort
@@ -86,17 +86,16 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
-    binding * class list -> tsig -> tsig
+  val add_class: Proof.context -> Name_Space.naming -> binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
   val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
   val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
-  val add_arity: Pretty.pp -> arity -> tsig -> tsig
-  val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
-  val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
+  val add_arity: Proof.context -> arity -> tsig -> tsig
+  val add_classrel: Proof.context -> class * class -> tsig -> tsig
+  val merge_tsig: Proof.context -> tsig * tsig -> tsig
 end;
 
 structure Type: TYPE =
@@ -116,15 +115,15 @@
   | strip_constraints (Abs (x, T, t)) = Abs (x, T, strip_constraints t)
   | strip_constraints a = a;
 
-fun appl_error pp (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
+fun appl_error ctxt (Const ("_type_constraint_", Type ("fun", [T, _]))) _ u U =
       cat_lines
        ["Failed to meet type constraint:", "",
         Pretty.string_of (Pretty.block
-         [Pretty.str "Term:", Pretty.brk 2, Pretty.term pp u,
-          Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U]),
+         [Pretty.str "Term:", Pretty.brk 2, Syntax.pretty_term ctxt u,
+          Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U]),
         Pretty.string_of (Pretty.block
-         [Pretty.str "Type:", Pretty.brk 2, Pretty.typ pp T])]
-  | appl_error pp t T u U =
+         [Pretty.str "Type:", Pretty.brk 2, Syntax.pretty_typ ctxt T])]
+  | appl_error ctxt t T u U =
       cat_lines
        ["Type error in application: " ^
           (case T of
@@ -132,11 +131,11 @@
           | _ => "operator not of function type"),
         "",
         Pretty.string_of (Pretty.block
-          [Pretty.str "Operator:", Pretty.brk 2, Pretty.term pp t,
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp T]),
+          [Pretty.str "Operator:", Pretty.brk 2, Syntax.pretty_term ctxt t,
+            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt T]),
         Pretty.string_of (Pretty.block
-          [Pretty.str "Operand:", Pretty.brk 3, Pretty.term pp u,
-            Pretty.str " ::", Pretty.brk 1, Pretty.typ pp U])];
+          [Pretty.str "Operand:", Pretty.brk 3, Syntax.pretty_term ctxt u,
+            Pretty.str " ::", Pretty.brk 1, Syntax.pretty_typ ctxt U])];
 
 
 
@@ -310,7 +309,7 @@
 
 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
-      handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
+      handle Sorts.CLASS_ERROR err => error (Sorts.class_error (Syntax.init_pretty pp) err);
 
 
 
@@ -577,14 +576,14 @@
 
 (* classes *)
 
-fun add_class ctxt pp naming (c, cs) tsig =
+fun add_class ctxt naming (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
       val _ = Binding.check c;
       val (c', space') = space |> Name_Space.declare ctxt true naming c;
-      val classes' = classes |> Sorts.add_class pp (c', cs');
+      val classes' = classes |> Sorts.add_class ctxt (c', cs');
     in ((space', classes'), default, types) end);
 
 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
@@ -593,7 +592,7 @@
 
 (* arities *)
 
-fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
+fun add_arity ctxt (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   let
     val _ =
       (case lookup_type tsig t of
@@ -602,18 +601,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 ctxt ((t, map (fn c' => (c', Ss')) S'));
   in ((space, classes'), default, types) end);
 
 
 (* classrel *)
 
-fun add_classrel pp rel tsig =
+fun add_classrel ctxt rel tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val rel' = pairself (cert_class tsig) rel
         handle TYPE (msg, _, _) => error msg;
-      val classes' = classes |> Sorts.add_classrel pp rel';
+      val classes' = classes |> Sorts.add_classrel ctxt rel';
     in ((space, classes'), default, types) end);
 
 
@@ -674,7 +673,7 @@
 
 (* merge type signatures *)
 
-fun merge_tsig pp (tsig1, tsig2) =
+fun merge_tsig ctxt (tsig1, tsig2) =
   let
     val (TSig {classes = (space1, classes1), default = default1, types = types1,
       log_types = _}) = tsig1;
@@ -682,7 +681,7 @@
       log_types = _}) = tsig2;
 
     val space' = Name_Space.merge (space1, space2);
-    val classes' = Sorts.merge_algebra pp (classes1, classes2);
+    val classes' = Sorts.merge_algebra ctxt (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 c9bf3f8a8930 -r 77eedb527068 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Pure/type_infer.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -217,10 +217,10 @@
 
 exception NO_UNIFIER of string * typ Vartab.table;
 
-fun unify ctxt pp =
+fun unify ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
 
 
     (* adjust sorts of parameters *)
@@ -289,9 +289,6 @@
 
 fun infer ctxt =
   let
-    val pp = Syntax.pp ctxt;
-
-
     (* errors *)
 
     fun prep_output tye bs ts Ts =
@@ -310,7 +307,7 @@
 
     fun err_appl msg tye bs t T u U =
       let val ([t', u'], [T', U']) = prep_output tye bs [t, u] [T, U]
-      in error (unif_failed msg ^ Type.appl_error pp t' T' u' U' ^ "\n") end;
+      in error (unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n") end;
 
 
     (* main *)
@@ -328,7 +325,7 @@
             val (T, tye_idx') = inf bs t tye_idx;
             val (U, (tye, idx)) = inf bs u tye_idx';
             val V = mk_param idx [];
-            val tye_idx'' = unify ctxt pp (U --> V, T) (tye, idx + 1)
+            val tye_idx'' = unify ctxt (U --> V, T) (tye, idx + 1)
               handle NO_UNIFIER (msg, tye') => err_appl msg tye' bs t T u U;
           in (V, tye_idx'') end;
 
diff -r c9bf3f8a8930 -r 77eedb527068 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -431,8 +431,7 @@
       |> fold (ensure_fun thy arities eqngr) cs
       |> fold (ensure_rhs thy arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
-    val pp = Syntax.pp_global thy;
-    val algebra = Sorts.subalgebra pp (is_proper_class thy)
+    val algebra = Sorts.subalgebra (Syntax.init_pretty_global thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
     val (rhss, eqngr') = Symtab.fold (add_cert thy vardeps) eqntab ([], eqngr);
     fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
diff -r c9bf3f8a8930 -r 77eedb527068 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -574,18 +574,25 @@
 fun translation_error thy permissive some_thm msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
-  else let
-    val err_thm = case some_thm
-     of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
-      | NONE => "";
-  in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+  else
+    let
+      val err_thm =
+        (case some_thm of
+          SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"
+        | NONE => "");
+    in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
 
 fun not_wellsorted thy permissive some_thm ty sort e =
   let
-    val err_class = Sorts.class_error (Syntax.pp_global thy) e;
-    val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
-      ^ Syntax.string_of_sort_global thy sort;
-  in translation_error thy permissive some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
+    val ctxt = Syntax.init_pretty_global thy;
+    val err_class = Sorts.class_error ctxt e;
+    val err_typ =
+      "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
+        Syntax.string_of_sort_global thy sort;
+  in
+    translation_error thy permissive some_thm "Wellsortedness error"
+      (err_typ ^ "\n" ^ err_class)
+  end;
 
 
 (* translation *)
diff -r c9bf3f8a8930 -r 77eedb527068 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Mon Apr 18 12:12:42 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon Apr 18 15:02:50 2011 +0200
@@ -98,8 +98,7 @@
 fun unify weak ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val pp = Syntax.pp ctxt;
-    val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy);
+    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
 
 
     (* adjust sorts of parameters *)
@@ -190,8 +189,8 @@
 
 (** error messages **)
 
-fun gen_msg err msg = 
-  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^ 
+fun gen_msg err msg =
+  err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
   (if msg = "" then "" else ": " ^ msg) ^ "\n";
 
 fun prep_output ctxt tye bs ts Ts =
@@ -204,27 +203,26 @@
   in (map prep ts', Ts') end;
 
 fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
-  
+
 fun unif_failed msg =
   "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
-  
+
 fun err_appl_msg ctxt msg tye bs t T u U () =
   let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
-  in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
+  in unif_failed msg ^ Type.appl_error ctxt t' T' u' U' ^ "\n" end;
 
 fun err_list ctxt msg tye Ts =
   let
     val (_, Ts') = prep_output ctxt tye [] [] Ts;
-    val text = cat_lines ([msg,
-      "Cannot unify a list of types that should be the same:",
-      (Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
+    val text =
+      msg ^ "\n" ^ "Cannot unify a list of types that should be the same:" ^ "\n" ^
+        Pretty.string_of (Pretty.list "[" "]" (map (Syntax.pretty_typ ctxt) Ts'));
   in
     error text
   end;
 
 fun err_bound ctxt msg tye packs =
   let
-    val pp = Syntax.pp ctxt;
     val (ts, Ts) = fold
       (fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
         let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
@@ -233,9 +231,10 @@
     val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
         (map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
           Pretty.block [
-            Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
-            Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
-            Pretty.block [Pretty.term pp (t $ u)]]))
+            Syntax.pretty_typ ctxt T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2,
+            Syntax.pretty_typ ctxt U, Pretty.brk 3,
+            Pretty.str "from function application", Pretty.brk 2,
+            Pretty.block [Syntax.pretty_term ctxt (t $ u)]]))
         ts Ts))
   in
     error text
@@ -277,21 +276,20 @@
 
 fun process_constraints ctxt err cs tye_idx =
   let
+    val thy = Proof_Context.theory_of ctxt;
+
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
-    val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
-    val pp = Syntax.pp ctxt;
-    val arity_sorts = Type.arity_sorts pp tsig;
-    val subsort = Type.subsort tsig;
+    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
 
     fun split_cs _ [] = ([], [])
       | split_cs f (c :: cs) =
           (case pairself f (fst c) of
             (false, false) => apsnd (cons c) (split_cs f cs)
           | _ => apfst (cons c) (split_cs f cs));
-          
+
     fun unify_list (T :: Ts) tye_idx =
-      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;      
+      fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
 
 
     (* check whether constraint simplification will terminate using weak unification *)
@@ -317,12 +315,12 @@
                 COVARIANT => (constraint :: cs, tye_idx)
               | CONTRAVARIANT => (swap constraint :: cs, tye_idx)
               | INVARIANT_TO T => (cs, unify_list [T, fst constraint, snd constraint] tye_idx
-                  handle NO_UNIFIER (msg, _) => 
-                    err_list ctxt (gen_msg err 
-                      "failed to unify invariant arguments w.r.t. to the known map function") 
+                  handle NO_UNIFIER (msg, _) =>
+                    err_list ctxt (gen_msg err
+                      "failed to unify invariant arguments w.r.t. to the known map function")
                       (fst tye_idx) Ts)
               | INVARIANT => (cs, strong_unify ctxt constraint tye_idx
-                  handle NO_UNIFIER (msg, _) => 
+                  handle NO_UNIFIER (msg, _) =>
                     error (gen_msg err ("failed to unify invariant arguments" ^ msg))));
             val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
               (fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
@@ -359,7 +357,7 @@
             val (ch, done') = split_cs (test_update o Type_Infer.deref tye') done;
             val todo' = ch @ todo;
           in
-            if subsort (S', S) (*TODO check this*)
+            if Sign.subsort thy (S', S) (*TODO check this*)
             then simplify done' todo' (tye', idx)
             else error (gen_msg err "sort mismatch")
           end
@@ -394,11 +392,11 @@
     (* do simplification *)
 
     val (cs', tye_idx') = simplify_constraints cs tye_idx;
-    
-    fun find_error_pack lower T' = map_filter 
+
+    fun find_error_pack lower T' = map_filter
       (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
-      
-    fun find_cycle_packs nodes = 
+
+    fun find_cycle_packs nodes =
       let
         val (but_last, last) = split_last nodes
         val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
@@ -431,7 +429,7 @@
         fun adjust T U = if super then (T, U) else (U, T);
         fun styp_test U Ts = forall
           (fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts;
-        fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts
+        fun fitting Ts S U = Sign.of_sort thy (t_of U, S) andalso styp_test U Ts
       in
         forall (fn (Ts, S) => exists (fitting Ts S) (T :: styps super T)) styps_and_sorts
       end;
@@ -448,7 +446,7 @@
     *)
     fun tightest sup S styps_and_sorts (T :: Ts) =
       let
-        fun restriction T = Type.of_sort tsig (t_of T, S)
+        fun restriction T = Sign.of_sort thy (t_of T, S)
           andalso ex_styp_of_sort (not sup) T styps_and_sorts;
         fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
       in
@@ -467,11 +465,11 @@
             val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
               handle Typ_Graph.CYCLES cycles =>
                 let
-                  val (tye, idx) = 
-                    fold 
+                  val (tye, idx) =
+                    fold
                       (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
-                        handle NO_UNIFIER (msg, _) => 
-                          err_bound ctxt 
+                        handle NO_UNIFIER (msg, _) =>
+                          err_bound ctxt
                             (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
                             (find_cycle_packs cycle)))
                       cycles tye_idx
@@ -495,13 +493,13 @@
           in
             if not (is_typeT T) orelse not (is_typeT U) orelse T = U
             then if super then (hd nodes, T') else (T', hd nodes)
-            else 
-              if super andalso 
+            else
+              if super andalso
                 Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
-              else if not super andalso 
+              else if not super andalso
                 Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
               else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
-                    (fst tye_idx) 
+                    (fst tye_idx)
                     (maps find_cycle_packs cycles @ find_error_pack super T')
           end;
       in
@@ -528,7 +526,7 @@
           val assignment =
             if null bound orelse null not_params then NONE
             else SOME (tightest lower S styps_and_sorts (map nameT not_params)
-                handle BOUND_ERROR msg => 
+                handle BOUND_ERROR msg =>
                   err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
         in
           (case assignment of
@@ -560,7 +558,7 @@
           val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
             |> fold (assign_ub G) ts;
         in
-          assign_alternating ts 
+          assign_alternating ts
             (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
         end;
 
@@ -573,7 +571,7 @@
           filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
         val to_unify = map (fn T => T :: get_preds G T) max_params;
       in
-        fold 
+        fold
           (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
             handle NO_UNIFIER (msg, _) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
           to_unify tye_idx
@@ -686,24 +684,24 @@
             val (u', U, (tye, idx)) = inf bs u tye_idx';
             val V = Type_Infer.mk_param idx [];
             val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
-              handle NO_UNIFIER (msg, tye') => 
+              handle NO_UNIFIER (msg, tye') =>
                 raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
           in (tu, V, tye_idx'') end;
 
-    fun infer_single t tye_idx = 
+    fun infer_single t tye_idx =
       let val (t, _, tye_idx') = inf [] t tye_idx;
       in (t, tye_idx') end;
-      
+
     val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
-      handle TYPE_INFERENCE_ERROR err =>     
+      handle TYPE_INFERENCE_ERROR err =>
         let
           fun gen_single t (tye_idx, constraints) =
             let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
             in (tye_idx', constraints' @ constraints) end;
-      
+
           val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
           val (tye, idx) = process_constraints ctxt err constraints tye_idx;
-        in 
+        in
           (insert_coercions ctxt tye ts, (tye, idx))
         end);
 
@@ -739,15 +737,15 @@
     val ctxt = Context.proof_of context;
     val t = singleton (Variable.polymorphic ctxt) raw_t;
 
-    fun err_str t = "\n\nThe provided function has the type\n" ^ 
-      Syntax.string_of_typ ctxt (fastype_of t) ^ 
+    fun err_str t = "\n\nThe provided function has the type\n" ^
+      Syntax.string_of_typ ctxt (fastype_of t) ^
       "\n\nThe general type signature of a map function is" ^
       "\nf1 => f2 => ... => fn => C [x1, ..., xn] => C [y1, ..., yn]" ^
       "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)";
-      
+
     val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
       handle Empty => error ("Not a proper map function:" ^ err_str t);
-    
+
     fun gen_arg_var ([], []) = []
       | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =
           if U = U' then
@@ -756,8 +754,8 @@
           else if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us)
           else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us)
           else error ("Functions do not apply to arguments correctly:" ^ err_str t)
-      | gen_arg_var (_, Ts) = 
-          if forall (op = andf is_stypeT o fst) Ts 
+      | gen_arg_var (_, Ts) =
+          if forall (op = andf is_stypeT o fst) Ts
           then map (INVARIANT_TO o fst) Ts
           else error ("Different numbers of functions and variant arguments\n" ^ err_str t);