equal
deleted
inserted
replaced
879 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
879 (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args)))) |
880 else list_comb ((build_aux f), (map build_aux args))) |
880 else list_comb ((build_aux f), (map build_aux args))) |
881 end |
881 end |
882 | build_aux x = |
882 | build_aux x = |
883 if is_const x then maybe_mk_rep_abs x else x |
883 if is_const x then maybe_mk_rep_abs x else x |
884 val prems = (*map HOLogic.dest_Trueprop*) (Thm.prems_of thm); |
884 val concl2 = term_of (#prop (crep_thm thm)) |
885 val concl = (*HOLogic.dest_Trueprop*) (Thm.concl_of thm); |
|
886 val concl2 = Logic.list_implies (prems, concl) |
|
887 (* val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*) |
|
888 in |
885 in |
889 Logic.mk_equals ( (build_aux concl2), concl2) |
886 Logic.mk_equals ((build_aux concl2), concl2) |
890 end *} |
887 end *} |
891 |
888 |
892 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
889 ML {* val emptyt = (symmetric (unlam_def @{context} @{thm EMPTY_def})) *} |
893 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
890 ML {* val in_t = (symmetric (unlam_def @{context} @{thm IN_def})) *} |
894 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |
891 ML {* val uniont = symmetric (unlam_def @{context} @{thm UNION_def}) *} |