equal
deleted
inserted
replaced
711 fun TERMFUN |
711 fun TERMFUN |
712 (fun_over_terms : term list * term -> 'a) |
712 (fun_over_terms : term list * term -> 'a) |
713 (i_opt : int option) : thm -> 'a list = fn st => |
713 (i_opt : int option) : thm -> 'a list = fn st => |
714 let |
714 let |
715 val t_raws = |
715 val t_raws = |
716 Thm.rep_thm st |
716 Thm.prop_of st |
717 |> #prop |
|
718 |> strip_top_all_vars [] |
717 |> strip_top_all_vars [] |
719 |> snd |
718 |> snd |
720 |> Logic.strip_horn |
719 |> Logic.strip_horn |
721 |> fst |
720 |> fst |
722 in |
721 in |