merge
authorblanchet
Fri, 24 Sep 2010 11:36:28 +0200
changeset 39673 fabd6b48fe6e
parent 39672 a89040dd6416 (diff)
parent 39671 6fcd95367c67 (current diff)
child 39675 b4cbc72a354c
merge
--- a/src/Tools/Metis/metis.ML	Fri Sep 24 10:31:42 2010 +0200
+++ b/src/Tools/Metis/metis.ML	Fri Sep 24 11:36:28 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
 
--- a/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 10:31:42 2010 +0200
+++ b/src/Tools/Metis/src/Rewrite.sml	Fri Sep 24 11:36:28 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
--- a/src/Tools/Metis/src/Rule.sml	Fri Sep 24 10:31:42 2010 +0200
+++ b/src/Tools/Metis/src/Rule.sml	Fri Sep 24 11:36:28 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