# HG changeset patch
# User blanchet
# Date 1284681379 -7200
# Node ID aaa7078fff55d497d80d72981289e5d34e0991dd
# Parent  d91ef7fbc5004b9a7fe96f225823e028715d4eee
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)

diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Active.sig
--- a/src/Tools/Metis/src/Active.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Active.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE ACTIVE SET OF CLAUSES                                                 *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Active =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Active.sml
--- a/src/Tools/Metis/src/Active.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Active.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE ACTIVE SET OF CLAUSES                                                 *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Active :> Active =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Atom.sig
--- a/src/Tools/Metis/src/Atom.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC ATOMS                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Atom =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Atom.sml
--- a/src/Tools/Metis/src/Atom.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Atom.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC ATOMS                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Atom :> Atom =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/AtomNet.sig
--- a/src/Tools/Metis/src/AtomNet.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature AtomNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/AtomNet.sml
--- a/src/Tools/Metis/src/AtomNet.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/AtomNet.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure AtomNet :> AtomNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Clause.sig
--- a/src/Tools/Metis/src/Clause.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* CLAUSE = ID + THEOREM                                                     *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Clause =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Clause.sml
--- a/src/Tools/Metis/src/Clause.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Clause.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* CLAUSE = ID + THEOREM                                                     *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Clause :> Clause =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/ElementSet.sig
--- a/src/Tools/Metis/src/ElementSet.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature ElementSet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/ElementSet.sml
--- a/src/Tools/Metis/src/ElementSet.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/ElementSet.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 functor ElementSet (KM : KeyMap) :> ElementSet
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Formula.sig
--- a/src/Tools/Metis/src/Formula.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC FORMULAS                                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Formula =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Formula.sml
--- a/src/Tools/Metis/src/Formula.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Formula.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC FORMULAS                                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Formula :> Formula =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Heap.sig
--- a/src/Tools/Metis/src/Heap.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A HEAP DATATYPE FOR ML                                                    *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Heap =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Heap.sml
--- a/src/Tools/Metis/src/Heap.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Heap.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A HEAP DATATYPE FOR ML                                                    *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Heap :> Heap =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/KeyMap.sig
--- a/src/Tools/Metis/src/KeyMap.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature KeyMap =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/KeyMap.sml
--- a/src/Tools/Metis/src/KeyMap.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KeyMap.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/KnuthBendixOrder.sig
--- a/src/Tools/Metis/src/KnuthBendixOrder.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE KNUTH-BENDIX TERM ORDERING                                            *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature KnuthBendixOrder =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/KnuthBendixOrder.sml
--- a/src/Tools/Metis/src/KnuthBendixOrder.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/KnuthBendixOrder.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* KNUTH-BENDIX TERM ORDERING CONSTRAINTS                                    *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure KnuthBendixOrder :> KnuthBendixOrder =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Lazy.sig
--- a/src/Tools/Metis/src/Lazy.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SUPPORT FOR LAZY EVALUATION                                               *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Lazy =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Lazy.sml
--- a/src/Tools/Metis/src/Lazy.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Lazy.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SUPPORT FOR LAZY EVALUATION                                               *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Lazy :> Lazy =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Literal.sig
--- a/src/Tools/Metis/src/Literal.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC LITERALS                                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Literal =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Literal.sml
--- a/src/Tools/Metis/src/Literal.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Literal.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC LITERALS                                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Literal :> Literal =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/LiteralNet.sig
--- a/src/Tools/Metis/src/LiteralNet.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature LiteralNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/LiteralNet.sml
--- a/src/Tools/Metis/src/LiteralNet.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/LiteralNet.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC LITERALS           *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure LiteralNet :> LiteralNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Map.sig
--- a/src/Tools/Metis/src/Map.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Map.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Map =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Map.sml
--- a/src/Tools/Metis/src/Map.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Map.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Map :> Map =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Model.sig
--- a/src/Tools/Metis/src/Model.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Model.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* RANDOM FINITE MODELS                                                      *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Model =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Model.sml
--- a/src/Tools/Metis/src/Model.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Model.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* RANDOM FINITE MODELS                                                      *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Model :> Model =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Name.sig
--- a/src/Tools/Metis/src/Name.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Name.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NAMES                                                                     *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Name =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Name.sml
--- a/src/Tools/Metis/src/Name.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Name.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NAMES                                                                     *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Name :> Name =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/NameArity.sig
--- a/src/Tools/Metis/src/NameArity.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NAME/ARITY PAIRS                                                          *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature NameArity =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/NameArity.sml
--- a/src/Tools/Metis/src/NameArity.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/NameArity.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NAME/ARITY PAIRS                                                          *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure NameArity :> NameArity =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Normalize.sig
--- a/src/Tools/Metis/src/Normalize.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NORMALIZING FORMULAS                                                      *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Normalize =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Normalize.sml
--- a/src/Tools/Metis/src/Normalize.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Normalize.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* NORMALIZING FORMULAS                                                      *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Normalize :> Normalize =
@@ -685,24 +685,23 @@
 (* Basic conjunctive normal form.                                            *)
 (* ------------------------------------------------------------------------- *)
 
-val newSkolemFunction =
-    let
-      val counter : int StringMap.map ref = ref (StringMap.new ())
+local
+  val counter : int StringMap.map ref = ref (StringMap.new ());
 
-      fun new n () =
-          let
-            val ref m = counter
-            val s = Name.toString n
-            val i = Option.getOpt (StringMap.peek m s, 0)
-            val () = counter := StringMap.insert m (s, i + 1)
-            val i = if i = 0 then "" else "_" ^ Int.toString i
-            val s = skolemPrefix ^ "_" ^ s ^ i
-          in
-            Name.fromString s
-          end
-    in
-      fn n => Portable.critical (new n) ()
-    end;
+  fun new n () =
+      let
+        val ref m = counter
+        val s = Name.toString n
+        val i = Option.getOpt (StringMap.peek m s, 0)
+        val () = counter := StringMap.insert m (s, i + 1)
+        val i = if i = 0 then "" else "_" ^ Int.toString i
+        val s = skolemPrefix ^ "_" ^ s ^ i
+      in
+        Name.fromString s
+      end;
+in
+  fun newSkolemFunction n = Portable.critical (new n) ();
+end;
 
 fun skolemize fv bv fm =
     let
@@ -1241,18 +1240,19 @@
 (* Definitions.                                                              *)
 (* ------------------------------------------------------------------------- *)
 
-val newDefinitionRelation =
-    let
-      val counter : int ref = ref 0
-    in
-      fn () => Portable.critical (fn () =>
-         let
-           val ref i = counter
-           val () = counter := i + 1
-         in
-           definitionPrefix ^ "_" ^ Int.toString i
-         end) ()
-    end;
+local
+  val counter : int ref = ref 0;
+
+  fun new () =
+      let
+        val ref i = counter
+        val () = counter := i + 1
+      in
+        definitionPrefix ^ "_" ^ Int.toString i
+      end;
+in
+  fun newDefinitionRelation () = Portable.critical new ();
+end;
 
 fun newDefinition def =
     let
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Options.sig
--- a/src/Tools/Metis/src/Options.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Options.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PROCESSING COMMAND LINE OPTIONS                                           *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Options =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Options.sml
--- a/src/Tools/Metis/src/Options.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Options.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PROCESSING COMMAND LINE OPTIONS                                           *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Options :> Options =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Ordered.sig
--- a/src/Tools/Metis/src/Ordered.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ORDERED TYPES                                                             *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Ordered =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Ordered.sml
--- a/src/Tools/Metis/src/Ordered.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Ordered.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ORDERED TYPES                                                             *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure IntOrdered =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Parse.sig
--- a/src/Tools/Metis/src/Parse.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PARSING                                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Parse =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Parse.sml
--- a/src/Tools/Metis/src/Parse.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Parse.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PARSING                                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Parse :> Parse =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Portable.sig
--- a/src/Tools/Metis/src/Portable.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Portable.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ML COMPILER SPECIFIC FUNCTIONS                                            *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Portable =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/PortableMlton.sml
--- a/src/Tools/Metis/src/PortableMlton.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortableMlton.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MLTON SPECIFIC FUNCTIONS                                                  *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Portable :> Portable =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/PortableMosml.sml
--- a/src/Tools/Metis/src/PortableMosml.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortableMosml.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MOSCOW ML SPECIFIC FUNCTIONS                                              *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Portable :> Portable =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/PortablePolyml.sml
--- a/src/Tools/Metis/src/PortablePolyml.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/PortablePolyml.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* POLY/ML SPECIFIC FUNCTIONS                                                *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Portable :> Portable =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Print.sig
--- a/src/Tools/Metis/src/Print.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Print.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PRETTY-PRINTING                                                           *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Print =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Print.sml
--- a/src/Tools/Metis/src/Print.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Print.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PRETTY-PRINTING                                                           *)
-(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Print :> Print =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Problem.sig
--- a/src/Tools/Metis/src/Problem.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* CNF PROBLEMS                                                              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Problem =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Problem.sml
--- a/src/Tools/Metis/src/Problem.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Problem.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* CNF PROBLEMS                                                              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Problem :> Problem =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Proof.sig
--- a/src/Tools/Metis/src/Proof.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PROOFS IN FIRST ORDER LOGIC                                               *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Proof =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Proof.sml
--- a/src/Tools/Metis/src/Proof.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Proof.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PROOFS IN FIRST ORDER LOGIC                                               *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Proof :> Proof =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Resolution.sig
--- a/src/Tools/Metis/src/Resolution.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE RESOLUTION PROOF PROCEDURE                                            *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Resolution =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Resolution.sml
--- a/src/Tools/Metis/src/Resolution.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Resolution.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE RESOLUTION PROOF PROCEDURE                                            *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Resolution :> Resolution =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Rewrite.sig
--- a/src/Tools/Metis/src/Rewrite.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ORDERED REWRITING FOR FIRST ORDER TERMS                                   *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Rewrite =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Rewrite.sml
--- a/src/Tools/Metis/src/Rewrite.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ORDERED REWRITING FOR FIRST ORDER TERMS                                   *)
-(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Rewrite :> Rewrite =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Rule.sig
--- a/src/Tools/Metis/src/Rule.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Rule =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Rule.sml
--- a/src/Tools/Metis/src/Rule.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* DERIVED RULES FOR CREATING FIRST ORDER LOGIC THEOREMS                     *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Rule :> Rule =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Set.sig
--- a/src/Tools/Metis/src/Set.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Set.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Set =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Set.sml
--- a/src/Tools/Metis/src/Set.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Set.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Set :> Set =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Sharing.sig
--- a/src/Tools/Metis/src/Sharing.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PRESERVING SHARING OF ML VALUES                                           *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Sharing =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Sharing.sml
--- a/src/Tools/Metis/src/Sharing.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Sharing.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* PRESERVING SHARING OF ML VALUES                                           *)
-(* Copyright (c) 2005 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2005 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Sharing :> Sharing =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Stream.sig
--- a/src/Tools/Metis/src/Stream.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Stream =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Stream.sml
--- a/src/Tools/Metis/src/Stream.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Stream.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Stream :> Stream =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Subst.sig
--- a/src/Tools/Metis/src/Subst.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Subst =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Subst.sml
--- a/src/Tools/Metis/src/Subst.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Subst :> Subst =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Subsume.sig
--- a/src/Tools/Metis/src/Subsume.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES                        *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Subsume =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Subsume.sml
--- a/src/Tools/Metis/src/Subsume.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Subsume.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES                        *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Subsume :> Subsume =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Term.sig
--- a/src/Tools/Metis/src/Term.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Term.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC TERMS                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Term =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Term.sml
--- a/src/Tools/Metis/src/Term.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Term.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC TERMS                                                   *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Term :> Term =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/TermNet.sig
--- a/src/Tools/Metis/src/TermNet.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature TermNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/TermNet.sml
--- a/src/Tools/Metis/src/TermNet.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/TermNet.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure TermNet :> TermNet =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Thm.sig
--- a/src/Tools/Metis/src/Thm.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Thm =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Thm.sml
--- a/src/Tools/Metis/src/Thm.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Thm.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Thm :> Thm =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Tptp.sig
--- a/src/Tools/Metis/src/Tptp.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE TPTP PROBLEM FILE FORMAT                                              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Tptp =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Tptp.sml
--- a/src/Tools/Metis/src/Tptp.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE TPTP PROBLEM FILE FORMAT                                              *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Tptp :> Tptp =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Units.sig
--- a/src/Tools/Metis/src/Units.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Units.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A STORE FOR UNIT THEOREMS                                                 *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Units =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Units.sml
--- a/src/Tools/Metis/src/Units.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Units.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* A STORE FOR UNIT THEOREMS                                                 *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Units :> Units =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Useful.sig
--- a/src/Tools/Metis/src/Useful.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ML UTILITY FUNCTIONS                                                      *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Useful =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Useful.sml
--- a/src/Tools/Metis/src/Useful.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Useful.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* ML UTILITY FUNCTIONS                                                      *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Useful :> Useful =
@@ -462,50 +462,33 @@
 end;
 
 local
-  fun calcPrimes ps n i =
-      if List.exists (fn p => divides p i) ps then calcPrimes ps n (i + 1)
+  fun calcPrimes mode ps i n =
+      if n = 0 then ps
+      else if List.exists (fn p => divides p i) ps then
+        let
+          val i = i + 1
+          and n = if mode then n else n - 1
+        in
+          calcPrimes mode ps i n
+        end
       else
         let
           val ps = ps @ [i]
+          and i = i + 1
           and n = n - 1
         in
-          if n = 0 then ps else calcPrimes ps n (i + 1)
+          calcPrimes mode ps i n
         end;
-
-  val primesList = ref [2];
 in
-  fun primes n = Portable.critical (fn () =>
-      let
-        val ref ps = primesList
-
-        val k = n - length ps
-      in
-        if k <= 0 then List.take (ps,n)
-        else
-          let
-            val ps = calcPrimes ps k (List.last ps + 1)
+  fun primes n =
+      if n <= 0 then []
+      else calcPrimes true [2] 3 (n - 1);
 
-            val () = primesList := ps
-          in
-            ps
-          end
-      end) ();
+  fun primesUpTo n =
+      if n < 2 then []
+      else calcPrimes false [2] 3 (n - 2);
 end;
 
-fun primesUpTo n = Portable.critical (fn () =>
-    let
-      fun f k =
-          let
-            val l = primes k
-
-            val p = List.last l
-          in
-            if p < n then f (2 * k) else takeWhile (fn j => j <= n) l
-          end
-    in
-      f 8
-    end) ();
-
 (* ------------------------------------------------------------------------- *)
 (* Strings.                                                                  *)
 (* ------------------------------------------------------------------------- *)
@@ -723,23 +706,30 @@
 
 local
   val generator = ref 0
-in
-  fun newInt () = Portable.critical (fn () =>
+
+  fun newIntThunk () =
       let
         val n = !generator
+
         val () = generator := n + 1
       in
         n
-      end) ();
+      end;
 
-  fun newInts 0 = []
-    | newInts k = Portable.critical (fn () =>
+  fun newIntsThunk k () =
       let
         val n = !generator
+
         val () = generator := n + k
       in
         interval n k
-      end) ();
+      end;
+in
+  fun newInt () = Portable.critical newIntThunk ();
+
+  fun newInts k =
+      if k <= 0 then []
+      else Portable.critical (newIntsThunk k) ();
 end;
 
 fun withRef (r,new) f x =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Waiting.sig
--- a/src/Tools/Metis/src/Waiting.sig	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sig	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE WAITING SET OF CLAUSES                                                *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 signature Waiting =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/Waiting.sml
--- a/src/Tools/Metis/src/Waiting.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/Waiting.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* THE WAITING SET OF CLAUSES                                                *)
-(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2002 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 structure Waiting :> Waiting =
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/metis.sml
--- a/src/Tools/Metis/src/metis.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/metis.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* METIS FIRST ORDER PROVER                                                  *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 open Useful;
@@ -13,7 +13,7 @@
 
 val VERSION = "2.3";
 
-val versionString = PROGRAM^" "^VERSION^" (release 20100915)"^"\n";
+val versionString = PROGRAM^" "^VERSION^" (release 20100916)"^"\n";
 
 (* ------------------------------------------------------------------------- *)
 (* Program options.                                                          *)
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/problems.sml
--- a/src/Tools/Metis/src/problems.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/problems.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 (* ========================================================================= *)
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/problems2tptp.sml
--- a/src/Tools/Metis/src/problems2tptp.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/problems2tptp.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* SOME SAMPLE PROBLEMS TO TEST PROOF PROCEDURES                             *)
-(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 open Useful;
diff -r d91ef7fbc500 -r aaa7078fff55 src/Tools/Metis/src/selftest.sml
--- a/src/Tools/Metis/src/selftest.sml	Fri Sep 17 01:22:01 2010 +0200
+++ b/src/Tools/Metis/src/selftest.sml	Fri Sep 17 01:56:19 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* METIS TESTS                                                               *)
-(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License            *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the MIT license            *)
 (* ========================================================================= *)
 
 (* ------------------------------------------------------------------------- *)