| changeset 56619 | e9726f630a83 |
| parent 56435 | 28b34e8e4a80 |
| child 57832 | 5b48f2047c24 |
--- a/src/Pure/ML-Systems/polyml.ML Sat Apr 19 17:23:05 2014 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sat Apr 19 17:28:07 2014 +0200 @@ -72,8 +72,6 @@ (* pervasive environment *) -fun op before (a, _: unit) = a; - val _ = PolyML.Compiler.forgetValue "isSome"; val _ = PolyML.Compiler.forgetValue "getOpt"; val _ = PolyML.Compiler.forgetValue "valOf";