equal
deleted
inserted
replaced
45 |
45 |
46 val cong_hd = fst o dest_Const o head_of o fst o Logic.dest_equals o concl_of; |
46 val cong_hd = fst o dest_Const o head_of o fst o Logic.dest_equals o concl_of; |
47 |
47 |
48 fun add_cong(congs,thm) = |
48 fun add_cong(congs,thm) = |
49 let val c = cong_hd thm |
49 let val c = cong_hd thm |
50 in case assoc(congs,c) of None => (c,thm)::congs |
50 in overwrite_warn (congs,(c,thm)) |
51 | _ => (warning ("Overwriting congruence rule for " ^ quote c); |
51 ("Overwriting congruence rule for " ^ quote c) |
52 overwrite (congs, (c,thm))) |
|
53 end |
52 end |
54 |
53 |
55 fun del_cong(congs,thm) = |
54 fun del_cong(congs,thm) = |
56 let val c = cong_hd thm |
55 let val c = cong_hd thm |
57 val (del, rest) = partition (fn (n, _) => n = c) congs |
56 val (del, rest) = partition (fn (n, _) => n = c) congs |