--- a/Admin/isatest/settings/at-poly-test Tue Feb 08 18:39:36 2011 +0100
+++ b/Admin/isatest/settings/at-poly-test Wed Feb 09 08:42:23 2011 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
POLYML_HOME="/home/polyml/polyml-svn"
- ML_SYSTEM="polyml-5.3.0"
+ ML_SYSTEM="polyml-5.4.1"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/Admin/isatest/settings/at-sml-dev-e Tue Feb 08 18:39:36 2011 +0100
+++ b/Admin/isatest/settings/at-sml-dev-e Wed Feb 09 08:42:23 2011 +0100
@@ -2,7 +2,7 @@
# Standard ML of New Jersey 110 or later
ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.67/bin"
+ML_HOME="/home/smlnj/110.72/bin"
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
--- a/Admin/isatest/settings/at64-poly Tue Feb 08 18:39:36 2011 +0100
+++ b/Admin/isatest/settings/at64-poly Wed Feb 09 08:42:23 2011 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.3.0"
- ML_SYSTEM="polyml-5.3.0"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86_64-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 1000"
--- a/Admin/isatest/settings/mac-poly Tue Feb 08 18:39:36 2011 +0100
+++ b/Admin/isatest/settings/mac-poly Wed Feb 09 08:42:23 2011 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.3.0-old"
- ML_SYSTEM="polyml-5.3.0"
+ POLYML_HOME="/home/polyml/polyml-5.2.1"
+ ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="ppc-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/NEWS Tue Feb 08 18:39:36 2011 +0100
+++ b/NEWS Wed Feb 09 08:42:23 2011 +0100
@@ -13,6 +13,9 @@
* Discontinued support for Poly/ML 5.2, which was the last version
without proper multithreading and TimeLimit implementation.
+* Discontinued old lib/scripts/polyml-platform, which has been
+obsolete since Isabelle2009-2.
+
*** HOL ***
--- a/lib/scripts/polyml-platform Tue Feb 08 18:39:36 2011 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-echo "### Legacy feature: polyml-platform script is superseded by ISABELLE_PLATFORM" >&2
-echo "$ISABELLE_PLATFORM"
--- a/src/HOL/Typedef.thy Tue Feb 08 18:39:36 2011 +0100
+++ b/src/HOL/Typedef.thy Wed Feb 09 08:42:23 2011 +0100
@@ -9,10 +9,6 @@
uses ("Tools/typedef.ML")
begin
-ML {*
-structure HOL = struct val thy = @{theory HOL} end;
-*} -- "belongs to theory HOL"
-
locale type_definition =
fixes Rep and Abs and A
assumes Rep: "Rep x \<in> A"
--- a/src/Pure/ProofGeneral/pgip_types.ML Tue Feb 08 18:39:36 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Feb 09 08:42:23 2011 +0100
@@ -273,7 +273,7 @@
| Pgipbool => "pgipbool"
| Pgipint _ => "pgipint"
| Pgipnat => "pgipint"
- | Pgipreal => "pgipint" (* FIXME sic? *)
+ | Pgipreal => "pgipint" (*sic!*) (*required for PG 4.0 and 3.7.x*)
| Pgipstring => "pgipstring"
| Pgipconst _ => "pgipconst"
| Pgipchoice _ => "pgipchoice"