# HG changeset patch
# User wenzelm
# Date 1320610665 -3600
# Node ID e99fd663c4a3c3bcdd91ca1a072827ab1c951684
# Parent  ccec8b6d5d81559267eaa70af0dd6d309586987e
tuned;

diff -r ccec8b6d5d81 -r e99fd663c4a3 src/Pure/Isar/class.ML
--- 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