diff -r a7e6ac2dfa58 -r 913162a47d9f src/Tools/Metis/scripts/mlpp
--- a/src/Tools/Metis/scripts/mlpp	Wed Jul 08 16:35:23 2020 +0200
+++ b/src/Tools/Metis/scripts/mlpp	Thu Jul 09 11:39:16 2020 +0200
@@ -1,6 +1,6 @@
 #!/usr/bin/perl
 
-# Copyright (c) 2006 Joe Hurd, distributed under the BSD License
+# Copyright (c) 2006 Joe Leslie-Hurd, distributed under the BSD License
 
 use strict;
 use warnings;
@@ -72,19 +72,7 @@
     my $text = shift @_;
 
     if ($opt_c eq "mosml") {
-        $text =~ s/Array\.copy/Array_copy/g;
-        $text =~ s/Array\.foldli/Array_foldli/g;
-        $text =~ s/Array\.foldri/Array_foldri/g;
-        $text =~ s/Array\.modifyi/Array_modifyi/g;
-        $text =~ s/OS\.Process\.isSuccess/OS_Process_isSuccess/g;
-        $text =~ s/PP\.ppstream/ppstream/g;
-        $text =~ s/String\.concatWith/String_concatWith/g;
-        $text =~ s/String\.isSubstring/String_isSubstring/g;
-        $text =~ s/String\.isSuffix/String_isSuffix/g;
-        $text =~ s/Substring\.full/Substring_full/g;
-        $text =~ s/TextIO\.inputLine/TextIO_inputLine/g;
-        $text =~ s/Vector\.foldli/Vector_foldli/g;
-        $text =~ s/Vector\.mapi/Vector_mapi/g;
+        $text =~ s/Real\.isFinite/Real_isFinite/g;
     }
 
     print STDOUT $text;
@@ -300,7 +288,7 @@
 
 =head1 AUTHORS
 
-Joe Hurd <joe@gilith.com>
+Joe Leslie-Hurd <joe@gilith.com>
 
 =head1 SEE ALSO