obsolete since polyml-5.5.0;
authorwenzelm
Sat, 19 Apr 2014 17:28:07 +0200
changeset 56619 e9726f630a83
parent 56618 874bdedb2313
child 56620 5de64a07b0e3
obsolete since polyml-5.5.0;
src/Pure/ML-Systems/polyml.ML
--- 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";