1.1 --- a/Admin/isatest/settings/at-poly-test	Tue Feb 08 18:39:36 2011 +0100
     1.2 +++ b/Admin/isatest/settings/at-poly-test	Wed Feb 09 08:42:23 2011 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  # -*- shell-script -*- :mode=shellscript:
     1.5  
     1.6    POLYML_HOME="/home/polyml/polyml-svn"
     1.7 -  ML_SYSTEM="polyml-5.3.0"
     1.8 +  ML_SYSTEM="polyml-5.4.1"
     1.9    ML_PLATFORM="x86-linux"
    1.10    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.11    ML_OPTIONS="-H 500"

     2.1 --- a/Admin/isatest/settings/at-sml-dev-e	Tue Feb 08 18:39:36 2011 +0100
     2.2 +++ b/Admin/isatest/settings/at-sml-dev-e	Wed Feb 09 08:42:23 2011 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4  
     2.5  # Standard ML of New Jersey 110 or later
     2.6  ML_SYSTEM=smlnj
     2.7 -ML_HOME="/home/smlnj/110.67/bin"
     2.8 +ML_HOME="/home/smlnj/110.72/bin"
     2.9  ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
    2.10  ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
    2.11  

     3.1 --- a/Admin/isatest/settings/at64-poly	Tue Feb 08 18:39:36 2011 +0100
     3.2 +++ b/Admin/isatest/settings/at64-poly	Wed Feb 09 08:42:23 2011 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  # -*- shell-script -*- :mode=shellscript:
     3.5  
     3.6 -  POLYML_HOME="/home/polyml/polyml-5.3.0"
     3.7 -  ML_SYSTEM="polyml-5.3.0"
     3.8 +  POLYML_HOME="/home/polyml/polyml-5.2.1"
     3.9 +  ML_SYSTEM="polyml-5.2.1"
    3.10    ML_PLATFORM="x86_64-linux"
    3.11    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    3.12    ML_OPTIONS="-H 1000"

     4.1 --- a/Admin/isatest/settings/mac-poly	Tue Feb 08 18:39:36 2011 +0100
     4.2 +++ b/Admin/isatest/settings/mac-poly	Wed Feb 09 08:42:23 2011 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  # -*- shell-script -*- :mode=shellscript:
     4.5  
     4.6 -  POLYML_HOME="/home/polyml/polyml-5.3.0-old"
     4.7 -  ML_SYSTEM="polyml-5.3.0"
     4.8 +  POLYML_HOME="/home/polyml/polyml-5.2.1"
     4.9 +  ML_SYSTEM="polyml-5.2.1"
    4.10    ML_PLATFORM="ppc-darwin"
    4.11    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    4.12    ML_OPTIONS="-H 500"

     5.1 --- a/NEWS	Tue Feb 08 18:39:36 2011 +0100
     5.2 +++ b/NEWS	Wed Feb 09 08:42:23 2011 +0100
     5.3 @@ -13,6 +13,9 @@
     5.4  * Discontinued support for Poly/ML 5.2, which was the last version
     5.5  without proper multithreading and TimeLimit implementation.
     5.6  
     5.7 +* Discontinued old lib/scripts/polyml-platform, which has been
     5.8 +obsolete since Isabelle2009-2.
     5.9 +
    5.10  
    5.11  *** HOL ***
    5.12  

     6.1 --- a/lib/scripts/polyml-platform	Tue Feb 08 18:39:36 2011 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,4 +0,0 @@
     6.4 -#!/usr/bin/env bash
     6.5 -
     6.6 -echo "### Legacy feature: polyml-platform script is superseded by ISABELLE_PLATFORM" >&2
     6.7 -echo "$ISABELLE_PLATFORM"

     7.1 --- a/src/HOL/Typedef.thy	Tue Feb 08 18:39:36 2011 +0100
     7.2 +++ b/src/HOL/Typedef.thy	Wed Feb 09 08:42:23 2011 +0100
     7.3 @@ -9,10 +9,6 @@
     7.4  uses ("Tools/typedef.ML")
     7.5  begin
     7.6  
     7.7 -ML {*
     7.8 -structure HOL = struct val thy = @{theory HOL} end;
     7.9 -*}  -- "belongs to theory HOL"
    7.10 -
    7.11  locale type_definition =
    7.12    fixes Rep and Abs and A
    7.13    assumes Rep: "Rep x \<in> A"

     8.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Tue Feb 08 18:39:36 2011 +0100
     8.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Feb 09 08:42:23 2011 +0100
     8.3 @@ -273,7 +273,7 @@
     8.4                      | Pgipbool => "pgipbool"
     8.5                      | Pgipint _ => "pgipint"
     8.6                      | Pgipnat => "pgipint"
     8.7 -                    | Pgipreal => "pgipint"  (* FIXME sic? *)
     8.8 +                    | Pgipreal => "pgipint"  (*sic!*)  (*required for PG 4.0 and 3.7.x*)
     8.9                      | Pgipstring => "pgipstring"
    8.10                      | Pgipconst _ => "pgipconst"
    8.11                      | Pgipchoice _ => "pgipchoice"