src/Tools/Metis/metis_env.ML
changeset 36692 54b64d4ad524
parent 33037 b22e44496dc2
     1.1 --- a/src/Tools/Metis/metis_env.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/Tools/Metis/metis_env.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  (* Metis-specific ML environment *)
     1.5 -nonfix ++ -- RL mem;
     1.6 +nonfix ++ -- RL;
     1.7  val explode = String.explode;
     1.8  val implode = String.implode;
     1.9  val print = TextIO.print;