src/HOL/Tools/TFL/casesplit.ML
changeset 32952 aeb1e44fbc19
parent 32727 9072201cd69d
child 36945 9bec62c10714
equal deleted inserted replaced
32951:83392f9d303f 32952:aeb1e44fbc19
   303 (* derive eqs, assuming strict, ie the rules have no assumptions = all
   303 (* derive eqs, assuming strict, ie the rules have no assumptions = all
   304    the well-foundness conditions have been solved. *)
   304    the well-foundness conditions have been solved. *)
   305 fun derive_init_eqs sgn rules eqs =
   305 fun derive_init_eqs sgn rules eqs =
   306   let
   306   let
   307     fun get_related_thms i =
   307     fun get_related_thms i =
   308       List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
   308       map_filter ((fn (r, x) => if x = i then SOME r else NONE));
   309     fun add_eq (i, e) xs =
   309     fun add_eq (i, e) xs =
   310       (e, (get_related_thms i rules), i) :: xs
   310       (e, (get_related_thms i rules), i) :: xs
   311     fun solve_eq (th, [], i) =
   311     fun solve_eq (th, [], i) =
   312           error "derive_init_eqs: missing rules"
   312           error "derive_init_eqs: missing rules"
   313       | solve_eq (th, [a], i) = (a, i)
   313       | solve_eq (th, [a], i) = (a, i)