# HG changeset patch # User wenzelm # Date 1527455747 -7200 # Node ID fb5653a7a8790cd7c10f389a82021b4a8a45e3bd # Parent cd8ab1a7a286006a7e627c95db5b560d396abec4 prefer existing operation; diff -r cd8ab1a7a286 -r fb5653a7a879 src/HOL/Library/case_converter.ML --- a/src/HOL/Library/case_converter.ML Sun May 27 22:37:08 2018 +0200 +++ b/src/HOL/Library/case_converter.ML Sun May 27 23:15:47 2018 +0200 @@ -15,9 +15,6 @@ if eq (k, k') then (SOME (k', v), kvs) else apsnd (cons (k', v)) (lookup_remove eq k kvs) -fun map_option _ NONE = NONE - | map_option f (SOME x) = SOME (f x) - fun mk_abort msg t = let val T = fastype_of t @@ -72,7 +69,7 @@ then SOME (End (body_type T)) else let - fun f (i, t) = term_to_coordinates P t |> map_option (pair i) + fun f (i, t) = term_to_coordinates P t |> Option.map (pair i) val tcos = map_filter I (map_index f args) in if null tcos then NONE @@ -474,7 +471,7 @@ val (typ_list, poss) = lhss |> Ctr_Sugar_Util.transpose |> map_index to_coordinates - |> map_filter (map_option add_T) + |> map_filter (Option.map add_T) |> flat |> split_list in