changeset 22878 | ca2eb5eb615b |
parent 22846 | fb79144af9a3 |
child 23634 | 55e579ef85aa |
--- 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));