src/Pure/tactical.ML
changeset 32187 cca43ca13f4f
parent 32169 fbada8ed12e6
child 32231 95b8afcbb0ed
     1.1 --- a/src/Pure/tactical.ML	Sat Jul 25 00:53:47 2009 +0200
     1.2 +++ b/src/Pure/tactical.ML	Sat Jul 25 10:31:27 2009 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  fun print_tac msg st =
     1.5   (tracing (msg ^ "\n" ^
     1.6      Pretty.string_of (Pretty.chunks
     1.7 -      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
     1.8 +      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
     1.9    Seq.single st);
    1.10  
    1.11  (*Pause until a line is typed -- if non-empty then fail. *)
    1.12 @@ -233,7 +233,7 @@
    1.13  fun tracify flag tac st =
    1.14    if !flag andalso not (!suppress_tracing) then
    1.15      (tracing (Pretty.string_of (Pretty.chunks
    1.16 -        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
    1.17 +        (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @
    1.18            [Pretty.str "** Press RETURN to continue:"])));
    1.19       exec_trace_command flag (tac, st))
    1.20    else tac st;