equal
deleted
inserted
replaced
299 let |
299 let |
300 val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value) |
300 val intros = map (Thm.prop_of o snd) ((#intros o rep_pred_data) value) |
301 in |
301 in |
302 fold Term.add_const_names intros [] |
302 fold Term.add_const_names intros [] |
303 |> (fn cs => |
303 |> (fn cs => |
304 if member (=) cs @{const_name "HOL.eq"} then |
304 if member (op =) cs @{const_name "HOL.eq"} then |
305 insert (op =) @{const_name Predicate.eq} cs |
305 insert (op =) @{const_name Predicate.eq} cs |
306 else cs) |
306 else cs) |
307 |> filter (fn c => (not (c = key)) andalso |
307 |> filter (fn c => (not (c = key)) andalso |
308 (is_inductive_predicate ctxt c orelse is_registered ctxt c)) |
308 (is_inductive_predicate ctxt c orelse is_registered ctxt c)) |
309 end; |
309 end; |