1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Oct 15 15:28:56 2012 +0200
1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Oct 15 15:43:12 2012 +0200
1.3 @@ -105,7 +105,6 @@
1.4
1.5 (** Proof Reconstruction **)
1.6
1.7 -(* prove row :: cell list -> tactic *)
1.8 fun prove_row (c :: cs) =
1.9 (case Lazy.force c of
1.10 Less thm =>
1.11 @@ -126,23 +125,23 @@
1.12 (Goal_Display.pretty_goal
1.13 {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
1.14
1.15 -fun row_index i = chr (i + 97)
1.16 -fun col_index j = string_of_int (j + 1)
1.17 +fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *)
1.18 +fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *)
1.19
1.20 -fun pr_unprovable_cell _ ((i,j), Less _) = ""
1.21 +fun pr_unprovable_cell _ ((i,j), Less _) = []
1.22 | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
1.23 - "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
1.24 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
1.25 | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
1.26 - "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
1.27 - ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
1.28 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
1.29 + "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
1.30 | pr_unprovable_cell ctxt ((i,j), False st) =
1.31 - "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
1.32 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
1.33
1.34 fun pr_unprovable_subgoals ctxt table =
1.35 table
1.36 |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
1.37 |> flat
1.38 - |> map (pr_unprovable_cell ctxt)
1.39 + |> maps (pr_unprovable_cell ctxt)
1.40
1.41 fun pr_cell (Less _ ) = " < "
1.42 | pr_cell (LessEq _) = " <="