equal
deleted
inserted
replaced
588 val concl = Logic.strip_assums_concl goal; |
588 val concl = Logic.strip_assums_concl goal; |
589 in |
589 in |
590 Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) |
590 Unify.smash_unifiers thy [(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule')) |
591 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') |
591 |> Seq.map (fn env => Drule.instantiate (dest_env thy env) rule') |
592 end |
592 end |
593 end handle Subscript => Seq.empty; |
593 end handle General.Subscript => Seq.empty; |
594 |
594 |
595 end; |
595 end; |
596 |
596 |
597 |
597 |
598 (* special renaming of rule parameters *) |
598 (* special renaming of rule parameters *) |