author | schirmer |
Tue, 06 Jul 2004 20:32:20 +0200 | |
changeset 15017 | 9ad392226da5 |
parent 15016 | bcbef8418da5 |
child 15018 | 0a84ca4e0f90 |
--- a/src/Pure/tctical.ML Tue Jul 06 20:31:37 2004 +0200 +++ b/src/Pure/tctical.ML Tue Jul 06 20:32:20 2004 +0200 @@ -198,7 +198,9 @@ fun print_tac msg = (fn st => (tracing msg; - Display.print_goals (! Display.goals_limit) st; Seq.single st)); + tracing ((Pretty.string_of o Pretty.chunks o + Display.pretty_goals (! Display.goals_limit)) st); + Seq.single st)); (*Pause until a line is typed -- if non-empty then fail. *) fun pause_tac st =