equal
deleted
inserted
replaced
90 |
90 |
91 |
91 |
92 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Set.member}, |
92 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Set.member}, |
93 @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"}, |
93 @{const_name "issued"}, @{const_name "cards"}, @{const_name "isin"}, |
94 @{const_name Collect}, @{const_name insert}] *} |
94 @{const_name Collect}, @{const_name insert}] *} |
95 ML {* Core_Data.force_modes_and_compilations *} |
95 ML_val {* Core_Data.force_modes_and_compilations *} |
96 |
96 |
97 fun find_first :: "('a => 'b option) => 'a list => 'b option" |
97 fun find_first :: "('a => 'b option) => 'a list => 'b option" |
98 where |
98 where |
99 "find_first f [] = None" |
99 "find_first f [] = None" |
100 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |
100 | "find_first f (x # xs) = (case f x of Some y => Some y | None => find_first f xs)" |