src/Pure/RAW/ml_name_space_polyml.ML
author wenzelm
Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337 d3996d5873dd
parent 61925 ab52f183f020
permissions -rw-r--r--
proper syntax;

(*  Title:      Pure/RAW/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;