--- 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