# HG changeset patch
# User blanchet
# Date 1285316831 -7200
# Node ID a89040dd6416b460e3cb1909e2e80b7c3792ac15
# Parent  9e3b035841e4ba3b4b4bca691a8b2152b93a197d
make SML/NJ happier -- temporary solution until Metis is fixed upstream

diff -r 9e3b035841e4 -r a89040dd6416 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Fri Sep 24 15:33:58 2010 +0900
+++ b/src/Tools/Metis/metis.ML	Fri Sep 24 10:27:11 2010 +0200
@@ -12752,7 +12752,7 @@
 
 fun ppEquation (_,th) = Metis_Thm.pp th;
 
-val equationToString = Metis_Print.toString ppEquation;
+fun equationToString x = Metis_Print.toString ppEquation x;
 
 fun equationLiteral (t_u,th) =
     let
@@ -18364,7 +18364,7 @@
         rw
       end;
 
-val addList = List.foldl (fn (eqn,rw) => add rw eqn);
+fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
 
 (* ------------------------------------------------------------------------- *)
 (* Rewriting (the order must be a refinement of the rewrite order).          *)
@@ -18824,7 +18824,7 @@
     end;
 end;
 
-val rewrite = orderedRewrite (K (SOME GREATER));
+fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
 
 end
 
diff -r 9e3b035841e4 -r a89040dd6416 src/Tools/Metis/src/Rewrite.sml
--- a/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 15:33:58 2010 +0900
+++ b/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 10:27:11 2010 +0200
@@ -207,7 +207,7 @@
         rw
       end;
 
-val addList = List.foldl (fn (eqn,rw) => add rw eqn);
+fun addList x = List.foldl (fn (eqn,rw) => add rw eqn) x;
 
 (* ------------------------------------------------------------------------- *)
 (* Rewriting (the order must be a refinement of the rewrite order).          *)
@@ -667,6 +667,6 @@
     end;
 end;
 
-val rewrite = orderedRewrite (K (SOME GREATER));
+fun rewrite x = orderedRewrite (K (SOME GREATER)) x;
 
 end
diff -r 9e3b035841e4 -r a89040dd6416 src/Tools/Metis/src/Rule.sml
--- a/src/Tools/Metis/src/Rule.sml	Fri Sep 24 15:33:58 2010 +0900
+++ b/src/Tools/Metis/src/Rule.sml	Fri Sep 24 10:27:11 2010 +0200
@@ -96,7 +96,7 @@
 
 fun ppEquation (_,th) = Thm.pp th;
 
-val equationToString = Print.toString ppEquation;
+fun equationToString x = Print.toString ppEquation x;
 
 fun equationLiteral (t_u,th) =
     let