src/Sequents/prover.ML
changeset 33049 c38f02fdf35d
parent 33038 8f9594c31de4
child 38500 d5477ee35820
equal deleted inserted replaced
33040:cffdb7b28498 33049:c38f02fdf35d
    29       (warning (cat_lines ("Ignoring duplicate theorems:" ::
    29       (warning (cat_lines ("Ignoring duplicate theorems:" ::
    30           map Display.string_of_thm_without_context dups));
    30           map Display.string_of_thm_without_context dups));
    31        dups);
    31        dups);
    32 
    32 
    33 fun (Pack(safes,unsafes)) add_safes ths   = 
    33 fun (Pack(safes,unsafes)) add_safes ths   = 
    34     let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,safes))
    34     let val dups = warn_duplicates (inter Thm.eq_thm_prop ths safes)
    35         val ths' = subtract Thm.eq_thm_prop dups ths
    35         val ths' = subtract Thm.eq_thm_prop dups ths
    36     in
    36     in
    37         Pack(sort (make_ord less) (ths'@safes), unsafes)
    37         Pack(sort (make_ord less) (ths'@safes), unsafes)
    38     end;
    38     end;
    39 
    39 
    40 fun (Pack(safes,unsafes)) add_unsafes ths = 
    40 fun (Pack(safes,unsafes)) add_unsafes ths = 
    41     let val dups = warn_duplicates (inter Thm.eq_thm_prop (ths,unsafes))
    41     let val dups = warn_duplicates (inter Thm.eq_thm_prop unsafes ths)
    42         val ths' = subtract Thm.eq_thm_prop dups ths
    42         val ths' = subtract Thm.eq_thm_prop dups ths
    43     in
    43     in
    44         Pack(safes, sort (make_ord less) (ths'@unsafes))
    44         Pack(safes, sort (make_ord less) (ths'@unsafes))
    45     end;
    45     end;
    46 
    46