diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 14e2806343234c1e3359e5cac5703ec6e5a276a8..63e59e9be9c783c9c4c157749d01fb0f6861e295 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -58,8 +58,8 @@ type formula =
   | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
   | CHC of formula * formula (* Choice is self-dual *)
   | FUS of bool * formula
-  | MU of formula * formula
-  | NU of formula * formula
+  | MU of string * formula
+  | NU of string * formula
   | VAR of string
   | AF of formula
   | EF of formula
@@ -231,17 +231,17 @@ let convertToMu formula =
 	let symbol = Stream.next gensym in
 	match formula with
 	| AF f1 ->
-	   MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+	   MU (symbol, (OR (f1, (AX ("", (VAR symbol))))))
 	| EF f1 ->
-	   MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+	   MU (symbol, (OR (f1, (EX ("", (VAR symbol))))))
 	| AG f1 ->
-	   NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+	   NU (symbol, (AND (f1, (AX ("", (VAR symbol))))))
 	| EG f1 ->
-	   NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+	   NU (symbol, (AND (f1, (EX ("", (VAR symbol))))))
 	| AU (f1, f2) ->
-	   MU ((VAR symbol), (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
+	   MU (symbol, (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
 	| EU (f1, f2) ->
-	   MU ((VAR symbol), (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
+	   MU (symbol, (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
 	| _ -> formula
   in
   convert_post helper formula
@@ -396,12 +396,12 @@ let rec exportFormula_buffer sb f =
       prio 4 f1
   | MU (s, f1) ->
       Buffer.add_string sb "μ";
-      prio 4 s;
+      Buffer.add_string sb s;
       Buffer.add_string sb ".";
       prio 4 f1
   | NU (s, f1) ->
       Buffer.add_string sb "ν";
-      prio 4 s;
+	  Buffer.add_string sb s;
       Buffer.add_string sb ".";
       prio 4 f1
   | VAR s ->
@@ -820,11 +820,11 @@ and parse_rest ts =
   | A.Kwd "μ" ->
       let (_, _, s) = boxinternals true "." in
       let f1 = parse_rest ts in
-      MU (VAR s, f1)
+      MU (s, f1)
   | A.Kwd "ν" ->
       let (_, _, s) = boxinternals true "." in
       let f1 = parse_rest ts in
-      NU (VAR s, f1)
+      NU (s, f1)
   | A.Kwd "AF" ->
 	  let f = parse_rest ts in
 	  AF f
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index c807b4ec96c332a85e19f9f0ae578307ee3b2e7b..b133f8671aa471b3c2d5aaaf7ba2bb8d65a9f755 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -41,8 +41,8 @@ type formula =
   | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
   | CHC of formula * formula
   | FUS of bool * formula
-  | MU of formula * formula
-  | NU of formula * formula
+  | MU of string * formula
+  | NU of string * formula
   | VAR of string
   | AF of formula
   | EF of formula