tuned;

--- a/src/Pure/Isar/class.ML	Sun Nov 06 18:42:17 2011 +0100
+++ b/src/Pure/Isar/class.ML	Sun Nov 06 21:17:45 2011 +0100
@@ -499,7 +499,6 @@
 fun pretty lthy =
   let
     val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
-    val thy = Proof_Context.theory_of lthy;
     fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
     fun pr_param ((c, _), (v, ty)) =
       Pretty.block (Pretty.breaks