diff --git a/ChangeLog b/ChangeLog
index 8eb5a2e41..8ec86ae62 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2004-05-14  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/tgbaalgos/neverclaim.cc (never_claim_bfs): Do not output
+	space before colon, and do not output the top-level formula using
+	Spin's syntax.
+
 2004-05-14  Thomas Martinez  <martinez@src.lip6.fr>
 
 	* src/tgbatest/ltl2tgba.cc (main): Thinko.
diff --git a/src/tgbaalgos/neverclaim.cc b/src/tgbaalgos/neverclaim.cc
index 95f68c054..22145702d 100644
--- a/src/tgbaalgos/neverclaim.cc
+++ b/src/tgbaalgos/neverclaim.cc
@@ -49,7 +49,7 @@ namespace spot
       if (f_)
         {
           os_ << " /* ";
-          to_spin_string(f_, os_);
+          to_string(f_, os_);
           os_ << " */";
         }
       os_ << std::endl;
@@ -63,7 +63,7 @@ namespace spot
         os_ << "  fi;" << std::endl;
       if (accept_all_ != -1)
         {
-          os_ << "accept_all :" << std::endl;
+          os_ << "accept_all:" << std::endl;
           os_ << "  skip" << std::endl;
         }
       os_ << "}" << std::endl;
@@ -125,7 +125,7 @@ namespace spot
         {
           if (fi_needed_ != 0)
             os_ << "  fi;" << std::endl;
-          os_ << get_state_label(s, n) << " : ";
+          os_ << get_state_label(s, n) << ": ";
           os_ << "/* " << automata_->format_state(s) << " */" ;
           os_ << std::endl;
           os_ << "  if" << std::endl;
@@ -144,7 +144,7 @@ namespace spot
             {
               if (fi_needed_)
                 os_ << "  fi;" << std::endl;
-              os_ << get_state_label(s, n) << " : ";
+              os_ << get_state_label(s, n) << ": ";
               os_ << "/* " << automata_->format_state(s) << " */";
               os_ << std::endl;
               os_ << "  if" << std::endl;