diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index b6c8fe3eeb5b7d3f6d93940d1fadc6f09d4bb809..84ca0d9c68f8bf2eb0200d827cc36b49b694fbd5 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -233,7 +233,7 @@ let rec propagateUnsat = function
                 let prop acc node =
                   match node with
                   | State state ->
-                      let turnsUnsat = 
+                      let turnsUnsat =
                         match stateGetStatus state with
                         | Expandable
                         | Open -> cssForall isConstraintUnsat (stateGetConstraints state)
@@ -476,9 +476,9 @@ let newCore sort bs =
         assert (okay1);
         let okay2 = M.add_clause solver [M.neg_lit lf; lf2] in
         assert (okay2)
-	| MuF
-	| NuF ->
-	   (*
+    | MuF
+    | NuF ->
+       (*
           Dest of a fixpoint is it's unfolded version. This adds just
           an simple forward implication that could be optimised out
           though not without nontrivial transformation of code
@@ -487,11 +487,11 @@ let newCore sort bs =
             φ[X |-> f]    |---> lf1
 
           Then adding lf -> lf1 to minisat
-		*)
-	   let f1 = lfGetDest1 sort f in
-	   addClauses f1;
-	   let lf1 = fhtMustFind fht f1 in
-	   let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
+        *)
+       let f1 = lfGetDest1 sort f in
+       addClauses f1;
+       let lf1 = fhtMustFind fht f1 in
+       let okay1 = M.add_clause solver [M.neg_lit lf; lf1] in
        assert (okay1);
     | _ -> ()
         (* case 2.(c)
@@ -560,10 +560,10 @@ let getNextState core =
           let lf2 = fhtMustFind fht f2 in
           assert (M.literal_status solver lf2 = M.LTRUE);
           mkExclClause f2 acc1
-	  | MuF
-	  | NuF ->
-		 let f1 = lfGetDest1 sort f in
-		 mkExclClause f1 acc
+      | MuF
+      | NuF ->
+         let f1 = lfGetDest1 sort f in
+         mkExclClause f1 acc
       | _ ->
           (* if f is a trivial formula or modality, then add it ... *)
           (* ... to newbs *)
@@ -748,7 +748,7 @@ let reasonerFinished () =
   | Unsat
   | Sat  -> true
   | Open -> queueIsEmpty ()
-    
+
 
 (** A graph-tableau-based decision procedure framework for coalgebraic logics.
     @param verbose An optional switch which determines
@@ -796,4 +796,3 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
     print_newline ()
   else ();
   sat
-