src/HOL/Tools/Function/lexicographic_order.ML
changeset 51958 bca32217b304
parent 51717 9e7d1c139569
child 56231 b98813774a63
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 06:50:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Mon May 13 12:40:17 2013 +0200
     1.3 @@ -120,22 +120,21 @@
     1.4  
     1.5  (** Error reporting **)
     1.6  
     1.7 -fun pr_goals ctxt st =
     1.8 -  Pretty.string_of
     1.9 -    (Goal_Display.pretty_goal
    1.10 -      {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
    1.11 -
    1.12  fun row_index i = chr (i + 97)  (* FIXME not scalable wrt. chr range *)
    1.13  fun col_index j = string_of_int (j + 1)  (* FIXME not scalable wrt. table layout *)
    1.14  
    1.15  fun pr_unprovable_cell _ ((i,j), Less _) = []
    1.16    | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
    1.17 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    1.18 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.19 +       Goal_Display.string_of_goal ctxt st]
    1.20    | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
    1.21 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
    1.22 -       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
    1.23 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.24 +       Goal_Display.string_of_goal ctxt st_less ^
    1.25 +       "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
    1.26 +       Goal_Display.string_of_goal ctxt st_leq]
    1.27    | pr_unprovable_cell ctxt ((i,j), False st) =
    1.28 -      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
    1.29 +      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
    1.30 +       Goal_Display.string_of_goal ctxt st]
    1.31  
    1.32  fun pr_unprovable_subgoals ctxt table =
    1.33    table