diff --git a/src/modelchecker.c b/src/modelchecker.c
index 09dd446..d77f478 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -32,13 +32,13 @@
    Some forward declarations.
 */
 
-__inline__ int traverseSimple (const System oldsys);
-__inline__ int traverseNonReads (const System oldsys);
-__inline__ int traversePOR4 (const System oldsys);
-__inline__ int traversePOR5 (const System oldsys);
-__inline__ int traversePOR6 (const System oldsys);
-__inline__ int traversePOR7 (const System oldsys);
-__inline__ int traversePOR8 (const System oldsys);
+int traverseSimple (const System oldsys);
+int traverseNonReads (const System oldsys);
+int traversePOR4 (const System oldsys);
+int traversePOR5 (const System oldsys);
+int traversePOR6 (const System oldsys);
+int traversePOR7 (const System oldsys);
+int traversePOR8 (const System oldsys);
 int propertyCheck (const System sys);
 int executeTry (const System sys, int run);
 int claimSecrecy (const System sys, const Term t);
diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index 26c29c1..c739b3f 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -357,7 +357,7 @@ prune_theorems (const System sys)
       b = bl->data;
 
       // Check for "Hidden" interm goals
-      //!@TODO in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
+      //! @todo in the future, this can be subsumed by adding TERM_Hidden to the hidelevel constructs
       if (termInTerm (b->term, TERM_Hidden))
 	{
 	  // Prune the state: we can never meet this
@@ -376,7 +376,7 @@ prune_theorems (const System sys)
 	  // Check for SK-type function occurrences
 	  //!@todo Needs a LEMMA, although this seems to be quite straightforward to prove.
 	  // The idea is that functions are never sent as a whole, but only used in applications.
-	  //!@TODO Subsumed by hidelevel lemma later
+	  //! @todo Subsumed by hidelevel lemma later
 	  if (isTermFunctionName (b->term))
 	    {
 	      if (!inKnowledge (sys->know, b->term))
@@ -397,7 +397,7 @@ prune_theorems (const System sys)
       // Check for encryption levels
       /*
        * if (switches.match < 2
-       *!@TODO Doesn't work yet as desired for Tickets. Prove lemma first.
+       *! @todo Doesn't work yet as desired for Tickets. Prove lemma first.
        */
       if (switches.experimental & 2)
 	{