| changeset 33037 | b22e44496dc2 |
| parent 33004 | 715566791eb0 |
| child 36692 | 54b64d4ad524 |
--- a/src/Tools/Metis/metis_env.ML Tue Oct 20 13:37:56 2009 +0200 +++ b/src/Tools/Metis/metis_env.ML Tue Oct 20 16:13:01 2009 +0200 @@ -1,5 +1,5 @@ (* Metis-specific ML environment *) -nonfix ++ -- RL mem union subset; +nonfix ++ -- RL mem; val explode = String.explode; val implode = String.implode; val print = TextIO.print;