equal
deleted
inserted
replaced
61 in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end; |
61 in (((cases, concls), consumes), Drule.cterm_instantiate substs rule) end; |
62 |
62 |
63 fun rename_params_rule internal xs rule = |
63 fun rename_params_rule internal xs rule = |
64 let |
64 let |
65 val tune = |
65 val tune = |
66 if internal then Term.internal |
66 if internal then Name.internal |
67 else fn x => the_default x (try Term.dest_internal x); |
67 else fn x => the_default x (try Name.dest_internal x); |
68 val n = length xs; |
68 val n = length xs; |
69 fun rename prem = |
69 fun rename prem = |
70 let |
70 let |
71 val ps = Logic.strip_params prem; |
71 val ps = Logic.strip_params prem; |
72 val p = length ps; |
72 val p = length ps; |