equal
deleted
inserted
replaced
26 |
26 |
27 val empty_pack = Pack([],[]); |
27 val empty_pack = Pack([],[]); |
28 |
28 |
29 fun warn_duplicates [] = [] |
29 fun warn_duplicates [] = [] |
30 | warn_duplicates dups = |
30 | warn_duplicates dups = |
31 (warning (String.concat ("Ignoring duplicate theorems:\n":: |
31 (warning (cat_lines ("Ignoring duplicate theorems:" :: map string_of_thm dups)); |
32 map (suffix "\n" o string_of_thm) dups)); |
|
33 dups); |
32 dups); |
34 |
33 |
35 fun (Pack(safes,unsafes)) add_safes ths = |
34 fun (Pack(safes,unsafes)) add_safes ths = |
36 let val dups = warn_duplicates (gen_inter eq_thm (ths,safes)) |
35 let val dups = warn_duplicates (gen_inter eq_thm (ths,safes)) |
37 val ths' = gen_rems eq_thm (ths,dups) |
36 val ths' = gen_rems eq_thm (ths,dups) |