tuned;

--- a/src/Pure/display.ML	Tue May 08 19:15:35 2007 +0200
+++ b/src/Pure/display.ML	Tue May 08 21:02:26 2007 +0200
@@ -80,7 +80,7 @@
     val tags = Thm.get_tags th;
 
     val q = if quote then Pretty.quote else I;
-    val prt_term = q o (Pretty.term pp);
+    val prt_term = q o Pretty.term pp;
 
     val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
     val ora' = ora andalso (! show_hyps orelse not (! quick_and_dirty));