30 | warn_duplicates dups = |
30 | warn_duplicates dups = |
31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups)); |
31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups)); |
32 dups); |
32 dups); |
33 |
33 |
34 fun (Pack(safes,unsafes)) add_safes ths = |
34 fun (Pack(safes,unsafes)) add_safes ths = |
35 let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,safes)) |
35 let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,safes)) |
36 val ths' = subtract Drule.eq_thm_prop dups ths |
36 val ths' = subtract Thm.eq_thm_prop dups ths |
37 in |
37 in |
38 Pack(sort (make_ord less) (ths'@safes), unsafes) |
38 Pack(sort (make_ord less) (ths'@safes), unsafes) |
39 end; |
39 end; |
40 |
40 |
41 fun (Pack(safes,unsafes)) add_unsafes ths = |
41 fun (Pack(safes,unsafes)) add_unsafes ths = |
42 let val dups = warn_duplicates (gen_inter Drule.eq_thm_prop (ths,unsafes)) |
42 let val dups = warn_duplicates (gen_inter Thm.eq_thm_prop (ths,unsafes)) |
43 val ths' = subtract Drule.eq_thm_prop dups ths |
43 val ths' = subtract Thm.eq_thm_prop dups ths |
44 in |
44 in |
45 Pack(safes, sort (make_ord less) (ths'@unsafes)) |
45 Pack(safes, sort (make_ord less) (ths'@unsafes)) |
46 end; |
46 end; |
47 |
47 |
48 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) = |
48 fun merge_pack (Pack(safes,unsafes), Pack(safes',unsafes')) = |