src/Pure/ML-Systems/polyml_old_basis.ML
changeset 29564 f8b933a62151
parent 28490 40c3f900c457
equal deleted inserted replaced
29563:4773c5c994dc 29564:f8b933a62151
     1 (*  Title:      Pure/ML-Systems/polyml_old_basis.ML
     1 (*  Title:      Pure/ML-Systems/polyml_old_basis.ML
     2     ID:         $Id$
       
     3 
     2 
     4 Fixes for the old SML basis library (before Poly/ML 4.2.0).
     3 Fixes for the old SML basis library (before Poly/ML 4.2.0).
     5 *)
     4 *)
     6 
     5 
     7 structure String =
     6 structure String =