equal
deleted
inserted
replaced
64 |
64 |
65 fun rename_params_rule internal xs rule = |
65 fun rename_params_rule internal xs rule = |
66 let |
66 let |
67 val tune = |
67 val tune = |
68 if internal then Name.internal |
68 if internal then Name.internal |
69 else fn x => the_default x (try Name.dest_internal x); |
69 else perhaps (try Name.dest_internal); |
70 val n = length xs; |
70 val n = length xs; |
71 fun rename prem = |
71 fun rename prem = |
72 let |
72 let |
73 val ps = Logic.strip_params prem; |
73 val ps = Logic.strip_params prem; |
74 val p = length ps; |
74 val p = length ps; |