# HG changeset patch
# User wenzelm
# Date 1397921287 -7200
# Node ID e9726f630a83ae45181a0925bdce34b79090fd0b
# Parent  874bdedb2313549b9b75a524c95296b2b0c6f070
obsolete since polyml-5.5.0;

diff -r 874bdedb2313 -r e9726f630a83 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";