equal
deleted
inserted
replaced
78 let |
78 let |
79 val (c, thm) = prep_cong raw_thm; |
79 val (c, thm) = prep_cong raw_thm; |
80 val (del, rest) = List.partition (Library.equal c o fst) congs; |
80 val (del, rest) = List.partition (Library.equal c o fst) congs; |
81 in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end; |
81 in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end; |
82 |
82 |
83 val add_congs = foldr (uncurry add_cong); |
|
84 |
|
85 end; |
83 end; |
86 |
84 |
87 |
85 |
88 |
86 |
89 (** global and local recdef data **) |
87 (** global and local recdef data **) |