376 that of the SML basis, which has constructors NONE and SOME instead of 
376 that of the SML basis, which has constructors NONE and SOME instead of 
377 None and Some, as well as exception Option.Option instead of OPTION. 
377 None and Some, as well as exception Option.Option instead of OPTION. 
378 The functions the, if_none, is_some, is_none have been adapted 
378 The functions the, if_none, is_some, is_none have been adapted 
379 accordingly, while Option.map replaces apsome. 
379 accordingly, while Option.map replaces apsome. 
380 
380 
381 * The exception LIST has been given up in favour of the standard 
381 * Pure/library.ML: the exception LIST has been given up in favour of 
382 exceptions Empty and Subscript, as well as Library.UnequalLengths. 
382 the standard exceptions Empty and Subscript, as well as 
383 Function like Library.hd and Library.tl are superceded by the standard 
383 Library.UnequalLengths. Function like Library.hd and Library.tl are 
384 hd and tl functions etc. 
384 superceded by the standard hd and tl functions etc. 
385 
385 
386 A number of basic functions are now no longer exported to the ML 
386 A number of basic list functions are no longer exported to the ML 
387 toplevel, as they are variants of standard functions. The following 
387 toplevel, as they are variants of predefined functions. The following 
388 suggests how one can translate existing code: 
388 suggests how one can translate existing code: 
389 
389 
390 rev_append xs ys = List.revAppend (xs, ys) 
390 rev_append xs ys = List.revAppend (xs, ys) 
391 nth_elem (i, xs) = List.nth (xs, i) 
391 nth_elem (i, xs) = List.nth (xs, i) 
392 last_elem xs = List.last xs 
392 last_elem xs = List.last xs 
393 flat xss = List.concat xss 
393 flat xss = List.concat xss 
394 seq fs = List.app fs 
394 seq fs = List.app fs 
395 partition P xs = List.partition P xs 
395 partition P xs = List.partition P xs 
396 filter P xs = List.filter P xs 

397 mapfilter f xs = List.mapPartial f xs 
396 mapfilter f xs = List.mapPartial f xs 

397 

398 * Pure/library.ML: several combinators for linear functional 

399 transformations, notably reverse application and composition: 

400 

401 x > f f #> g 

402 (x, y) > f f #> g 

403 

404 * Pure/library.ML: canonical list combinators fold, fold_rev, and 

405 fold_yield support linear functional transformations and nesting. For 

406 example: 

407 

408 fold f [x1, ..., xN] y = 

409 y > f x1 > ... > f xN 

410 

411 (fold o fold) f [xs1, ..., xsN] y = 

412 y > fold f xs1 > ... > fold f xsN 

413 

414 fold f [x1, ..., xN] = 

415 f x1 #> ... #> f xN 

416 

417 (fold o fold) f [xs1, ..., xsN] = 

418 fold f xs1 #> ... #> fold f xsN 

419 

420 * Pure/term.ML: combinators fold_atyps, fold_aterms, fold_term_types, 

421 fold_types traverse types/terms from left to right, observing 

422 canonical argument order. Supercedes previous foldl_XXX versions, 

423 add_frees, add_vars have been adapted as well: INCOMPATIBILITY. 
398 
424 
399 * Pure: output via the Isabelle channels of writeln/warning/error 
425 * Pure: output via the Isabelle channels of writeln/warning/error 
400 etc. is now passed through Output.output, with a hook for arbitrary 
426 etc. is now passed through Output.output, with a hook for arbitrary 
401 transformations depending on the print_mode (cf. Output.add_mode  
427 transformations depending on the print_mode (cf. Output.add_mode  
402 the first active mode that provides a output function wins). Already 
428 the first active mode that provides a output function wins). Already 