equal
deleted
inserted
replaced
1455 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1455 val (tpairs, Bs, Bi, C) = dest_state (state, i); |
1456 val iparams = map #1 (Logic.strip_params Bi); |
1456 val iparams = map #1 (Logic.strip_params Bi); |
1457 val short = length iparams - length cs; |
1457 val short = length iparams - length cs; |
1458 val newnames = |
1458 val newnames = |
1459 if short < 0 then error "More names than abstractions!" |
1459 if short < 0 then error "More names than abstractions!" |
1460 else Name.variant_list cs ((uncurry take) (short, iparams)) @ cs; |
1460 else Name.variant_list cs (take short iparams) @ cs; |
1461 val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; |
1461 val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi []; |
1462 val newBi = Logic.list_rename_params (newnames, Bi); |
1462 val newBi = Logic.list_rename_params (newnames, Bi); |
1463 in |
1463 in |
1464 (case duplicates (op =) cs of |
1464 (case duplicates (op =) cs of |
1465 a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state) |
1465 a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); state) |