# HG changeset patch
# User bulwahn
# Date 1297237343 -3600
# Node ID 02978b058ca94b9ac08a796dd845019bf23eacff
# Parent  bd7ee90267f27cd4700319e3ccc9d5febaf70641# Parent  d92cc39097e62617f9be9fe4fd2188199239174a
merged

diff -r bd7ee90267f2 -r 02978b058ca9 Admin/isatest/settings/at-poly-test
--- 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"
diff -r bd7ee90267f2 -r 02978b058ca9 Admin/isatest/settings/at-sml-dev-e
--- 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")
 
diff -r bd7ee90267f2 -r 02978b058ca9 Admin/isatest/settings/at64-poly
--- 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"
diff -r bd7ee90267f2 -r 02978b058ca9 Admin/isatest/settings/mac-poly
--- 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"
diff -r bd7ee90267f2 -r 02978b058ca9 NEWS
--- 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 ***
 
diff -r bd7ee90267f2 -r 02978b058ca9 lib/scripts/polyml-platform
--- 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"
diff -r bd7ee90267f2 -r 02978b058ca9 src/HOL/Typedef.thy
--- 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"
diff -r bd7ee90267f2 -r 02978b058ca9 src/Pure/ProofGeneral/pgip_types.ML
--- 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"