equal
deleted
inserted
replaced
656 | repair t = t |
656 | repair t = t |
657 val t' = t |> repair |> fold (curry absdummy) (map snd params) |
657 val t' = t |> repair |> fold (curry absdummy) (map snd params) |
658 fun do_instantiate th = |
658 fun do_instantiate th = |
659 let |
659 let |
660 val var = Term.add_vars (prop_of th) [] |
660 val var = Term.add_vars (prop_of th) [] |
661 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst) |
|
662 |> the_single |
661 |> the_single |
663 in th |> term_instantiate thy [(Var var, t')] end |
662 in th |> term_instantiate thy [(Var var, t')] end |
664 in |
663 in |
665 (etac @{thm allE} i |
664 (etac @{thm allE} i |
666 THEN rotate_tac ~1 i |
665 THEN rotate_tac ~1 i |