src/Sequents/prover.ML
changeset 7150 d203e2282789
parent 7122 87b233b31889
child 12123 739eba13e2cd
equal deleted inserted replaced
7149:d0c2168f7704 7150:d203e2282789
    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)