# HG changeset patch
# User wenzelm
# Date 1178650946 -7200
# Node ID ca2eb5eb615b07900dad0dfd7607751f8b78f505
# Parent  d53b72246e678e495c1d379f1cfa30de6ad920e1
tuned;

diff -r d53b72246e67 -r ca2eb5eb615b src/Pure/display.ML
--- 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));