src/HOL/Tools/Function/lexicographic_order.ML
changeset 32145 220c9e439d39
parent 32089 568a23753e3a
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 16:43:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 16:52:16 2009 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
     1.5  
     1.6  fun pr_goals ctxt st =
     1.7 -    Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st
     1.8 +    Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st
     1.9       |> Pretty.chunks
    1.10       |> Pretty.string_of
    1.11