!fresh_index
(* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "η" ^ string_of_int (fresh_id ())
+ (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
let rec freshen_term ?(index = ref 0) term =
let freshen_term = freshen_term ~index in