equal
deleted
inserted
replaced
73 val ps = Logic.strip_params prem; |
73 val ps = Logic.strip_params prem; |
74 val p = length ps; |
74 val p = length ps; |
75 val ys = |
75 val ys = |
76 if p < n then [] |
76 if p < n then [] |
77 else map (tune o #1) (take (p - n) ps) @ xs; |
77 else map (tune o #1) (take (p - n) ps) @ xs; |
78 in Logic.list_rename_params (ys, prem) end; |
78 in Logic.list_rename_params ys prem end; |
79 fun rename_prems prop = |
79 fun rename_prems prop = |
80 let val (As, C) = Logic.strip_horn prop |
80 let val (As, C) = Logic.strip_horn prop |
81 in Logic.list_implies (map rename As, C) end; |
81 in Logic.list_implies (map rename As, C) end; |
82 in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
82 in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
83 |
83 |