diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 4ee77971e4f7cb63ad5d8ad24b080b56f6e0a612..8b6863586b6519db29415bd9f963a6d66d2f9157 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -212,21 +212,25 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
   in
   convert_post helper formula
 
+let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
+
 let convertToMu formula =
-  let helper formula = match formula with
-  | AF f1 ->
-	 MU ((VAR ":genX"), (OR (f1, (AX ("", (VAR ":genX"))))))
-  | EF f1 ->
-	 MU ((VAR ":genX"), (OR (f1, (AX ("", (VAR ":genX"))))))
-  | AG f1 ->
-	 NU ((VAR ":genX"), (AND (f1, (AX ("", (VAR ":genX"))))))
-  | EG f1 ->
-	 NU ((VAR ":genX"), (AND (f1, (AX ("", (VAR ":genX"))))))
-  | AU (f1, f2) ->
-	 MU ((VAR ":genX"), (OR (f2, (AND (f1, (AX ("", (VAR ":genX"))))))))
-  | EU (f1, f2) ->
-	 MU ((VAR ":genX"), (OR (f2, (AND (f1, (EX ("", (VAR ":genX"))))))))
-  | _ -> formula
+  let helper formula =
+	let symbol = Stream.next gensym in
+	match formula with
+	| AF f1 ->
+	   MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+	| EF f1 ->
+	   MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+	| AG f1 ->
+	   NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+	| EG f1 ->
+	   NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+	| AU (f1, f2) ->
+	   MU ((VAR symbol), (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
+	| EU (f1, f2) ->
+	   MU ((VAR symbol), (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
+	| _ -> formula
   in
   convert_post helper formula