--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 16:43:31 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 16:52:16 2009 +0200
@@ -140,7 +140,7 @@
fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
fun pr_goals ctxt st =
- Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
+ Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
|> Pretty.chunks
|> Pretty.string_of