changeset 61925 | ab52f183f020 |
parent 61924 | 55b3d21ab5e5 |
child 61926 | 17ba31a2303b |
--- a/src/Pure/ML-Systems/ml_name_space_polyml.ML Wed Dec 23 21:15:26 2015 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* Title: Pure/ML-Systems/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;