--- a/Admin/isatest/settings/mac-poly64-M8 Mon Oct 15 16:18:48 2012 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8 Mon Oct 15 19:03:02 2012 +0200
@@ -2,8 +2,8 @@
init_components /home/isabelle/contrib "$HOME/admin/components/main"
- POLYML_HOME="/home/polyml/polyml-5.4.1"
- ML_SYSTEM="polyml-5.4.1"
+ POLYML_HOME="/home/polyml/polyml-5.5.0"
+ ML_SYSTEM="polyml-5.5.0"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 2000 --gcthreads 8"
--- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Oct 15 16:18:48 2012 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Oct 15 19:03:02 2012 +0200
@@ -105,7 +105,6 @@
(** Proof Reconstruction **)
-(* prove row :: cell list -> tactic *)
fun prove_row (c :: cs) =
(case Lazy.force c of
Less thm =>
@@ -126,23 +125,23 @@
(Goal_Display.pretty_goal
{main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
-fun row_index i = chr (i + 97)
-fun col_index j = string_of_int (j + 1)
+fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *)
+fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *)
-fun pr_unprovable_cell _ ((i,j), Less _) = ""
+fun pr_unprovable_cell _ ((i,j), Less _) = []
| pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
- "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
+ ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
| pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
- "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less
- ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq
+ ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
+ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
| pr_unprovable_cell ctxt ((i,j), False st) =
- "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st
+ ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
fun pr_unprovable_subgoals ctxt table =
table
|> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
|> flat
- |> map (pr_unprovable_cell ctxt)
+ |> maps (pr_unprovable_cell ctxt)
fun pr_cell (Less _ ) = " < "
| pr_cell (LessEq _) = " <="