src/Pure/RAW/ml_name_space_polyml.ML

--- a/src/Pure/RAW/ml_name_space_polyml.ML	Thu Mar 03 17:03:09 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  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;