diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/ml_name_space.ML
--- a/src/Pure/RAW/ml_name_space.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space.ML
-    Author:     Makarius
-
-ML name space -- dummy version of Poly/ML 5.2 facility.
-*)
-
-structure ML_Name_Space =
-struct
-
-type valueVal = unit;
-type typeVal = unit;
-type fixityVal = unit;
-type structureVal = unit;
-type signatureVal = unit;
-type functorVal = unit;
-
-type T =
- {lookupVal:    string -> valueVal option,
-  lookupType:   string -> typeVal option,
-  lookupFix:    string -> fixityVal option,
-  lookupStruct: string -> structureVal option,
-  lookupSig:    string -> signatureVal option,
-  lookupFunct:  string -> functorVal option,
-  enterVal:     string * valueVal -> unit,
-  enterType:    string * typeVal -> unit,
-  enterFix:     string * fixityVal -> unit,
-  enterStruct:  string * structureVal -> unit,
-  enterSig:     string * signatureVal -> unit,
-  enterFunct:   string * functorVal -> unit,
-  allVal:       unit -> (string * valueVal) list,
-  allType:      unit -> (string * typeVal) list,
-  allFix:       unit -> (string * fixityVal) list,
-  allStruct:    unit -> (string * structureVal) list,
-  allSig:       unit -> (string * signatureVal) list,
-  allFunct:     unit -> (string * functorVal) list};
-
-val global: T =
- {lookupVal = fn _ => NONE,
-  lookupType = fn _ => NONE,
-  lookupFix = fn _ => NONE,
-  lookupStruct = fn _ => NONE,
-  lookupSig = fn _ => NONE,
-  lookupFunct = fn _ => NONE,
-  enterVal = fn _ => (),
-  enterType = fn _ => (),
-  enterFix = fn _ => (),
-  enterStruct = fn _ => (),
-  enterSig = fn _ => (),
-  enterFunct = fn _ => (),
-  allVal = fn _ => [],
-  allType = fn _ => [],
-  allFix = fn _ => [],
-  allStruct = fn _ => [],
-  allSig = fn _ => [],
-  allFunct = fn _ => []};
-
-val initial_val : (string * valueVal) list = [];
-val initial_type : (string * typeVal) list = [];
-val initial_fixity : (string * fixityVal) list = [];
-val initial_structure : (string * structureVal) list = [];
-val initial_signature : (string * signatureVal) list = [];
-val initial_functor : (string * functorVal) list = [];
-
-fun forget_global_structure (_: string) = ();
-
-fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
-
-end;