--- a/src/Tools/Metis/metis.ML Sun Nov 08 13:56:44 2009 +0100
+++ b/src/Tools/Metis/metis.ML Sun Nov 08 13:57:07 2009 +0100
@@ -60,7 +60,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -102,10 +102,10 @@
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
-val randomWord = RandomWord.next_word;
-val randomBool = RandomWord.next_bool;
-fun randomInt n = RandomWord.next_int 0 (n - 1);
-val randomReal = RandomWord.next_real;
+val randomWord = Random_Word.next_word;
+val randomBool = Random_Word.next_bool;
+fun randomInt n = Random_Word.next_int 0 (n - 1);
+val randomReal = Random_Word.next_real;
end;
@@ -347,7 +347,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1274,7 +1274,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1979,7 +1979,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2061,7 +2061,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2200,7 +2200,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2820,7 +2820,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -3187,7 +3187,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -3823,7 +3823,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4106,7 +4106,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4297,7 +4297,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4550,7 +4550,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4787,7 +4787,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5293,7 +5293,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5565,7 +5565,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -5843,7 +5843,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -6622,7 +6622,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -6983,7 +6983,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -7423,7 +7423,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8117,7 +8117,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8554,7 +8554,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -8846,7 +8846,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -9521,7 +9521,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -10321,7 +10321,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -11493,7 +11493,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12157,7 +12157,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12408,7 +12408,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -12890,7 +12890,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13015,7 +13015,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13156,7 +13156,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13528,7 +13528,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -13882,7 +13882,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -14599,7 +14599,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -14826,7 +14826,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -15243,7 +15243,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16110,7 +16110,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16362,7 +16362,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -16563,7 +16563,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem union subset;
+nonfix ++ -- RL mem;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;