X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=60fe6357d5f1c4c878187f12e086c6ce49cd3006;hb=9e30dacbcdb10a58d6cf8f3995d1a195f2b31f4b;hp=48258d7bafffc17a66d23846cdc2f2fcdb1ceb35;hpb=046ba9f98a41651836720df1e9c2ebb6bd577ea9;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 48258d7ba..60fe6357d 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -362,7 +362,8 @@ let fresh_id () =
   !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