src/Pure/term.ML
changeset 17642 e063c0403650
parent 17314 04e21a27c0ad
child 17756 d4a35f82fbb4
equal deleted inserted replaced
17641:5ec55c1fa116 17642:e063c0403650
  1260 (* zero var indexes *)
  1260 (* zero var indexes *)
  1261 
  1261 
  1262 fun zero_var_inst vars =
  1262 fun zero_var_inst vars =
  1263   fold (fn v as ((x, i), X) => fn (used, inst) =>
  1263   fold (fn v as ((x, i), X) => fn (used, inst) =>
  1264     let
  1264     let
  1265       val x' = variant used x;
  1265       val x' = variant used (if is_bound x then "u" else x);
  1266       val used' = x' :: used;
  1266       val used' = x' :: used;
  1267     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
  1267     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
  1268   vars ([], []) |> #2;
  1268   vars ([], []) |> #2;
  1269 
  1269 
  1270 fun zero_var_indexesT ty =
  1270 fun zero_var_indexesT ty =