src/Pure/MLWorks.ML
1997-03-05 paulson 1997-03-05 Now declares needs_filtered_use, but still unusable with current MLWorks
1996-12-06 paulson 1996-12-06 MLWorks compatibility: it sort of works