changeset 32952 | aeb1e44fbc19 |
parent 32727 | 9072201cd69d |
child 36945 | 9bec62c10714 |
--- a/src/HOL/Tools/TFL/casesplit.ML Thu Oct 15 23:10:35 2009 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Thu Oct 15 23:28:10 2009 +0200 @@ -305,7 +305,7 @@ fun derive_init_eqs sgn rules eqs = let fun get_related_thms i = - List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE)); + map_filter ((fn (r, x) => if x = i then SOME r else NONE)); fun add_eq (i, e) xs = (e, (get_related_thms i rules), i) :: xs fun solve_eq (th, [], i) =