src/Pure/ML-Systems/ml_name_space_polyml.ML
author wenzelm
Sun, 20 Dec 2015 12:48:56 +0100
changeset 61874 a942e237c9e8
parent 61715 5dc95d957569
permissions -rw-r--r--
tuned;

(*  Title:      Pure/ML-Systems/ml_name_space_polyml.ML
    Author:     Makarius

Name space for Poly/ML.
*)

structure ML_Name_Space =
struct
  open PolyML.NameSpace;
  type T = nameSpace;
  val global = PolyML.globalNameSpace;
  val forget_global_structure = PolyML.Compiler.forgetStructure;
end;