src/Pure/General/same.ML
2009-07-16 ago added same;
2009-07-16 ago added map_option;
2009-07-16 ago added map;
2009-07-16 ago Support for copy-avoiding functions on pure values, at the cost of readability.