diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sat Apr 16 13:48:45 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Sat Apr 16 15:25:25 2011 +0200
@@ -158,11 +158,11 @@
 
 fun pretty lthy =
   let
-    val thy = ProofContext.theory_of lthy;
     val overloading = get_overloading lthy;
     fun pr_operation ((c, ty), (v, _)) =
-      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
-        Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty];
+      Pretty.block (Pretty.breaks
+        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
+          Pretty.str "::", Syntax.pretty_typ lthy ty]);
   in Pretty.str "overloading" :: map pr_operation overloading end;
 
 fun conclude lthy =