# HG changeset patch
# User wenzelm
# Date 1350320582 -7200
# Node ID 4a15873c4ec915cc50b3e3602fdcc3a338f0fcb5
# Parent  7bf407d77152b6710ea0149bd0aedae2b10d1848# Parent  2db80a0d76df24a963dd0ce3edefe4646fa9e4a1
merged

diff -r 7bf407d77152 -r 4a15873c4ec9 Admin/isatest/settings/mac-poly64-M8
--- 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"
diff -r 7bf407d77152 -r 4a15873c4ec9 src/HOL/Tools/Function/lexicographic_order.ML
--- 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 _) = " <="