equal
deleted
inserted
replaced
70 |
70 |
71 (** generic combinators **) |
71 (** generic combinators **) |
72 |
72 |
73 fun fold_consts f thms = |
73 fun fold_consts f thms = |
74 thms |
74 thms |
75 |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of) |
75 |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of) |
76 |> (fold o fold_aterms) (fn Const c => f c | _ => I); |
76 |> (fold o fold_aterms) (fn Const c => f c | _ => I); |
77 |
77 |
78 fun consts_of (const, []) = [] |
78 fun consts_of (const, []) = [] |
79 | consts_of (const, thms as thm :: _) = |
79 | consts_of (const, thms as thm :: _) = |
80 let |
80 let |