--- a/src/Pure/ML-Systems/ml_name_space_polyml-5.6.ML Wed Dec 23 21:15:26 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: Pure/ML-Systems/ml_name_space_polyml-5.6.ML
- Author: Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
-
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
- val forget_global_structure = PolyML.Compiler.forgetStructure;
-
- type valueVal = Values.value;
- fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
- fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-
- type typeVal = TypeConstrs.typeConstr;
- fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-
- type fixityVal = Infixes.fixity;
- fun displayFix (_: string, x) = Infixes.print x;
-
- type structureVal = Structures.structureVal;
- fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-
- type signatureVal = Signatures.signatureVal;
- fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-
- type functorVal = Functors.functorVal;
- fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-end;