equal
deleted
inserted
replaced
419 map (Name.internal o Name.clean o fst) (Logic.strip_params prem) |
419 map (Name.internal o Name.clean o fst) (Logic.strip_params prem) |
420 in Logic.list_rename_params xs prem end; |
420 in Logic.list_rename_params xs prem end; |
421 fun rename_prems prop = |
421 fun rename_prems prop = |
422 let val (As, C) = Logic.strip_horn prop |
422 let val (As, C) = Logic.strip_horn prop |
423 in Logic.list_implies (map rename As, C) end; |
423 in Logic.list_implies (map rename As, C) end; |
424 in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end; |
424 in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end; |
425 |
425 |
426 |
426 |
427 |
427 |
428 (** mutual_rule **) |
428 (** mutual_rule **) |
429 |
429 |