src/Pure/ML-Systems/polyml_common.ML

 val seconds = Time.fromReal;
 
 
 
 (** ML system and platform related **)
-
-val forget_structure = PolyML.Compiler.forgetStructure;
 
 val _ = PolyML.Compiler.forgetValue "isSome";
 val _ = PolyML.Compiler.forgetValue "getOpt";
 val _ = PolyML.Compiler.forgetValue "valOf";
 val _ = PolyML.Compiler.forgetValue "foldl";