--- a/src/Pure/RAW/ml_name_space.ML Wed Feb 17 21:08:18 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;