| NotationPt.Theorem (n, t, ty_opt, attrs) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
| NotationPt.Theorem (n, t, ty_opt, attrs) ->
let ty_opt =
match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
in
NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)