# 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