tuned;

--- a/src/Pure/sorts.ML	Fri Sep 25 19:20:24 2015 +0200
+++ b/src/Pure/sorts.ML	Fri Sep 25 19:23:17 2015 +0200
@@ -188,16 +188,16 @@
 
 fun err_dup_class c = error ("Duplicate declaration of class: " ^ quote c);
 
-fun err_cyclic_classes pp css =
+fun err_cyclic_classes context 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 (Syntax.init_pretty context) cs) css));
 
-fun add_class pp (c, cs) = map_classes (fn classes =>
+fun add_class context (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 context css;
   in classes'' end);
 
 
@@ -208,14 +208,14 @@
 fun for_classes _ NONE = ""
   | 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') =
-  let val ctxt = Syntax.init_pretty pp in
+fun err_conflict context t cc (c, Ss) (c', Ss') =
+  let val ctxt = Syntax.init_pretty context in
     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']))
   end;
 
-fun coregular pp algebra t (c, Ss) ars =
+fun coregular context algebra t (c, Ss) ars =
   let
     fun conflict (c', Ss') =
       if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
@@ -225,62 +225,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 context 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 context algebra t (c, Ss) ars =
   (case AList.lookup (op =) ars c of
-    NONE => coregular pp algebra t (c, Ss) ars
+    NONE => coregular context 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 context algebra t (c, Ss) (remove (op =) (c, Ss') ars)
+      else err_conflict context t NONE (c, Ss) (c, Ss'));
 
 in
 
-fun insert_ars pp algebra t = fold_rev (insert pp algebra t);
+fun insert_ars context algebra t = fold_rev (insert context algebra t);
 
-fun insert_complete_ars pp algebra (t, ars) arities =
+fun insert_complete_ars context 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 context 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 context arg algebra =
+  algebra |> map_arities (insert_complete_ars context algebra arg);
 
-fun add_arities_table pp algebra =
-  Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
+fun add_arities_table context algebra =
+  Symtab.fold (fn (t, ars) => insert_complete_ars context algebra (t, ars));
 
 end;
 
 
 (* classrel *)
 
-fun rebuild_arities pp algebra = algebra |> map_arities (fn arities =>
+fun rebuild_arities context algebra = algebra |> map_arities (fn arities =>
   Symtab.empty
-  |> add_arities_table pp algebra arities);
+  |> add_arities_table context algebra arities);
 
-fun add_classrel pp rel = rebuild_arities pp o map_classes (fn classes =>
+fun add_classrel context rel = rebuild_arities context 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 context css);
 
 
 (* empty and merge *)
 
 val empty_algebra = make_algebra (Graph.empty, Symtab.empty);
 
-fun merge_algebra pp
+fun merge_algebra context
    (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 context css;
     val algebra0 = make_algebra (classes', Symtab.empty);
     val arities' =
       (case (pointer_eq (classes1, classes2), pointer_eq (arities1, arities2)) of
@@ -288,20 +288,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 context algebra0 t ars2 ars1)
       | (false, true) =>  (*unary completion*)
           Symtab.empty
-          |> add_arities_table pp algebra0 arities1
+          |> add_arities_table context algebra0 arities1
       | (false, false) => (*binary completion*)
           Symtab.empty
-          |> add_arities_table pp algebra0 arities1
-          |> add_arities_table pp algebra0 arities2);
+          |> add_arities_table context algebra0 arities1
+          |> add_arities_table context 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 context 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) =
@@ -313,7 +313,7 @@
       else NONE;
     val classes' = classes |> Graph.restrict 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 context (make_algebra (classes', arities'))) end;
 
 
 
@@ -326,8 +326,8 @@
   No_Arity of string * class |
   No_Subsort of sort * sort;
 
-fun class_error pp =
-  let val ctxt = Syntax.init_pretty pp in
+fun class_error context =
+  let val ctxt = Syntax.init_pretty context in
     fn No_Classrel (c1, c2) => "No class relation " ^ Syntax.string_of_classrel ctxt [c1, c2]
      | No_Arity (a, c) => "No type arity " ^ Syntax.string_of_arity ctxt (a, [], [c])
      | No_Subsort (S1, S2) =>