pass plain Proof.context for pretty printing;

--- a/src/Pure/Isar/class.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/Isar/class.ML	Mon Apr 18 13:26:39 2011 +0200
@@ -530,7 +530,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 (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 =)

--- a/src/Pure/Isar/proof_context.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Apr 18 13:26:39 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 (Context.pretty 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 (Context.pretty ctxt) arity (tsig_of ctxt); arity end;
+  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
 
 in
 

--- a/src/Pure/sign.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/sign.ML	Mon Apr 18 13:26:39 2011 +0200
@@ -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;
 );
@@ -455,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 (Context.pretty 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 (Context.pretty_global thy) arg);
-fun primitive_arity arg thy = thy |> map_tsig (Type.add_arity (Context.pretty_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 *)

--- a/src/Pure/sorts.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/sorts.ML	Mon Apr 18 13:26:39 2011 +0200
@@ -40,12 +40,12 @@
   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: 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: 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: Context.pretty -> algebra * algebra -> algebra
-  val subalgebra: Context.pretty -> (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: Proof.context -> class_error -> string
@@ -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: " ^ Syntax.string_of_classrel (Syntax.init_pretty 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 " ^ Syntax.string_of_classrel (Syntax.init_pretty 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  " ^
-    Syntax.string_of_arity (Syntax.init_pretty pp) (t, Ss, [c]) ^ " and\n  " ^
-    Syntax.string_of_arity (Syntax.init_pretty 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;
 
 
 

--- a/src/Pure/type.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Pure/type.ML	Mon Apr 18 13:26:39 2011 +0200
@@ -86,17 +86,16 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Proof.context -> Context.pretty -> 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: 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: 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 =
@@ -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;

--- a/src/Tools/Code/code_preproc.ML	Mon Apr 18 12:11:58 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Mon Apr 18 13:26:39 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 = Context.pretty_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)