tuned;

--- a/src/Pure/type_infer.ML	Mon Apr 18 12:04:21 2011 +0200
+++ b/src/Pure/type_infer.ML	Mon Apr 18 12:11:58 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 = Context.pretty ctxt;
-
-
     (* errors *)
 
     fun prep_output tye bs ts Ts =
@@ -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;
 

--- a/src/Tools/subtyping.ML	Mon Apr 18 12:04:21 2011 +0200
+++ b/src/Tools/subtyping.ML	Mon Apr 18 12:11:58 2011 +0200
@@ -98,8 +98,7 @@
 fun unify weak ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val pp = Context.pretty 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 *)
@@ -280,8 +279,7 @@
     val coes_graph = coes_graph_of ctxt;
     val tmaps = tmaps_of ctxt;
     val tsig = Sign.tsig_of (Proof_Context.theory_of ctxt);
-    val pp = Context.pretty ctxt;
-    val arity_sorts = Type.arity_sorts pp tsig;
+    val arity_sorts = Type.arity_sorts (Context.pretty ctxt) tsig;
     val subsort = Type.subsort tsig;
 
     fun split_cs _ [] = ([], [])