diff --git a/src/claims.c b/src/claim.c
similarity index 99%
rename from src/claims.c
rename to src/claim.c
index e8ada33..31bc01f 100644
--- a/src/claims.c
+++ b/src/claim.c
@@ -1,5 +1,5 @@
 #include <stdlib.h>
-#include "termmaps.h"
+#include "termmap.h"
 #include "system.h"
 #include "error.h"
 
diff --git a/src/claims.h b/src/claim.h
similarity index 100%
rename from src/claims.h
rename to src/claim.h
diff --git a/src/compiler.c b/src/compiler.c
index a2e7912..bf192fe 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -1,13 +1,13 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include "tac.h"
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 #include "memory.h"
 #include "system.h"
 #include "knowledge.h"
-#include "symbols.h"
-#include "substitutions.h"
+#include "symbol.h"
+#include "substitution.h"
 #include "compiler.h"
 
 /*
diff --git a/src/constraints.c b/src/constraint.c
similarity index 99%
rename from src/constraints.c
rename to src/constraint.c
index 8400053..b745c1d 100644
--- a/src/constraints.c
+++ b/src/constraint.c
@@ -1,6 +1,6 @@
 #include <stdio.h>
 #include "memory.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "debug.h"
 #include "system.h"
 
diff --git a/src/constraints.h b/src/constraint.h
similarity index 98%
rename from src/constraints.h
rename to src/constraint.h
index ff5f541..5464cc9 100644
--- a/src/constraints.h
+++ b/src/constraint.h
@@ -1,6 +1,6 @@
 #ifndef CONSTRAINTS
 #define CONSTRAINTS
-#include "terms.h"
+#include "term.h"
 #include "knowledge.h"
 
 struct constraint
diff --git a/src/knowledge.c b/src/knowledge.c
index 700511f..85d26d7 100644
--- a/src/knowledge.c
+++ b/src/knowledge.c
@@ -6,7 +6,7 @@
  */
 #include <stdlib.h>
 #include <stdio.h>
-#include "termlists.h"
+#include "termlist.h"
 #include "knowledge.h"
 #include "memory.h"
 #include "system.h"
diff --git a/src/knowledge.h b/src/knowledge.h
index ac11252..38616f3 100644
--- a/src/knowledge.h
+++ b/src/knowledge.h
@@ -1,8 +1,8 @@
 #ifndef KNOWLEDGE
 #define KNOWLEDGE
 
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 
 //! Knowledge structure.
 /**
diff --git a/src/main.c b/src/main.c
index 7b1cbdf..a5d58b9 100644
--- a/src/main.c
+++ b/src/main.c
@@ -40,9 +40,9 @@
 #include "debug.h"
 #include "modelchecker.h"
 #include "memory.h"
-#include "symbols.h"
+#include "symbol.h"
 #include "pheading.h"
-#include "symbols.h"
+#include "symbol.h"
 #include "parser.h"
 #include "tac.h"
 #include "compiler.h"
diff --git a/src/match_basic.c b/src/match_basic.c
index b56ec19..d4afafa 100644
--- a/src/match_basic.c
+++ b/src/match_basic.c
@@ -8,7 +8,7 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include "memory.h"
-#include "substitutions.h"
+#include "substitution.h"
 #include "system.h"
 #include "modelchecker.h"
 #include "match_basic.h"
diff --git a/src/match_clp.c b/src/match_clp.c
index 1ac406c..8039732 100644
--- a/src/match_clp.c
+++ b/src/match_clp.c
@@ -12,7 +12,7 @@
 #include "match_clp.h"
 #include "system.h"
 #include "memory.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "mgu.h"
 #include "memory.h"
 #include "debug.h"
diff --git a/src/memory.c b/src/memory.c
index 44be6ed..6894576 100644
--- a/src/memory.c
+++ b/src/memory.c
@@ -22,10 +22,10 @@
 
 /* for displaying the sizes */
 
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 #include "knowledge.h"
-#include "substitutions.h"
+#include "substitution.h"
 #include "system.h"
 
 //! Open memory code.
diff --git a/src/mgu.c b/src/mgu.c
index 25281c1..8b3ad19 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -1,8 +1,8 @@
 #include <stdlib.h>
 #include <stdio.h>
-#include "terms.h"
-#include "termlists.h"
-#include "substitutions.h"
+#include "term.h"
+#include "termlist.h"
+#include "substitution.h"
 #include "mgu.h"
 #include "memory.h"
 
diff --git a/src/mgu.h b/src/mgu.h
index 5b65eef..045902f 100644
--- a/src/mgu.h
+++ b/src/mgu.h
@@ -1,9 +1,9 @@
 #ifndef MGU
 #define MGU
 
-#include "terms.h"
-#include "termlists.h"
-#include "substitutions.h"
+#include "term.h"
+#include "termlist.h"
+#include "substitution.h"
 
 //! A special constant do denote failure.
 /**
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 5354ee7..8733edc 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -7,7 +7,7 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
-#include "substitutions.h"
+#include "substitution.h"
 #include "knowledge.h"
 #include "system.h"
 #include "debug.h"
@@ -19,7 +19,7 @@
 #include "output.h"
 #include "tracebuf.h"
 #include "attackminimize.h"
-#include "claims.h"
+#include "claim.h"
 
 /*
 
diff --git a/src/pheading.h b/src/pheading.h
index a69c035..64a60cc 100644
--- a/src/pheading.h
+++ b/src/pheading.h
@@ -5,9 +5,9 @@
 
 #include <stdio.h>
 #include <stdlib.h>
-#include "terms.h"
-#include "termlists.h"
-#include "symbols.h"
+#include "term.h"
+#include "termlist.h"
+#include "symbol.h"
 #include "system.h"
 #include "tac.h"
 #endif
diff --git a/src/report.c b/src/report.c
index 20d1b53..2085db4 100644
--- a/src/report.c
+++ b/src/report.c
@@ -1,6 +1,6 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "terms.h"
+#include "term.h"
 #include "system.h"
 #include "debug.h"
 #include "output.h"
diff --git a/src/roles.c b/src/role.c
similarity index 97%
rename from src/roles.c
rename to src/role.c
index 6bdbcca..107f5b4 100644
--- a/src/roles.c
+++ b/src/role.c
@@ -5,16 +5,16 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 #include "knowledge.h"
 #include "system.h"
 #include "memory.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "debug.h"
 #include "output.h"
 #include "tracebuf.h"
-#include "roles.h"
+#include "role.h"
 
 extern int globalLatex;		// from system.c
 
diff --git a/src/roles.h b/src/role.h
similarity index 96%
rename from src/roles.h
rename to src/role.h
index 4295296..7c16aee 100644
--- a/src/roles.h
+++ b/src/role.h
@@ -1,11 +1,11 @@
 #ifndef ROLES
 #define ROLES
 
-#include "terms.h"
-#include "termmaps.h"
-#include "termlists.h"
+#include "term.h"
+#include "termmap.h"
+#include "termlist.h"
 #include "knowledge.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "states.h"
 
 #define	READ	1
diff --git a/src/substitutions.c b/src/substitution.c
similarity index 99%
rename from src/substitutions.c
rename to src/substitution.c
index 3fd2abb..a24bb80 100644
--- a/src/substitutions.c
+++ b/src/substitution.c
@@ -1,7 +1,7 @@
 #include <stdlib.h>
 #include <stdio.h>
-#include "terms.h"
-#include "substitutions.h"
+#include "term.h"
+#include "substitution.h"
 #include "memory.h"
 
 /* substitutions in terms */
diff --git a/src/substitutions.h b/src/substitution.h
similarity index 98%
rename from src/substitutions.h
rename to src/substitution.h
index 9fbb58b..c134ff4 100644
--- a/src/substitutions.h
+++ b/src/substitution.h
@@ -1,7 +1,7 @@
 #ifndef SUBSTITUTIONS
 #define SUBSTITUTIONS
 
-#include "termlists.h"
+#include "termlist.h"
 #include "knowledge.h"
 #include "system.h"
 
diff --git a/src/symbols.c b/src/symbol.c
similarity index 99%
rename from src/symbols.c
rename to src/symbol.c
index 4470088..ff8e4ff 100644
--- a/src/symbols.c
+++ b/src/symbol.c
@@ -1,7 +1,7 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-#include "symbols.h"
+#include "symbol.h"
 #include "memory.h"
 
 /*
diff --git a/src/symbols.h b/src/symbol.h
similarity index 100%
rename from src/symbols.h
rename to src/symbol.h
diff --git a/src/system.c b/src/system.c
index 3b5bcec..4f6a027 100644
--- a/src/system.c
+++ b/src/system.c
@@ -5,16 +5,16 @@
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 #include "knowledge.h"
 #include "system.h"
 #include "memory.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "debug.h"
 #include "output.h"
 #include "tracebuf.h"
-#include "roles.h"
+#include "role.h"
 
 /* from compiler.o */
 extern Term TERM_Type;
diff --git a/src/system.h b/src/system.h
index cc10b51..4640836 100644
--- a/src/system.h
+++ b/src/system.h
@@ -1,13 +1,13 @@
 #ifndef SYSTEM
 #define SYSTEM
 
-#include "terms.h"
-#include "termmaps.h"
-#include "termlists.h"
+#include "term.h"
+#include "termmap.h"
+#include "termlist.h"
 #include "knowledge.h"
-#include "constraints.h"
+#include "constraint.h"
 #include "states.h"
-#include "roles.h"
+#include "role.h"
 
 #define runPointerGet(sys,run)		sys->runs[run].index
 #define runPointerSet(sys,run,newp)	sys->runs[run].index = newp
diff --git a/src/tac.h b/src/tac.h
index 138e754..a8cf871 100644
--- a/src/tac.h
+++ b/src/tac.h
@@ -1,7 +1,7 @@
 #ifndef TAC_H
 #define TAC_H
 
-#include "symbols.h"
+#include "symbol.h"
 
 /*
  * TAC instructions
diff --git a/src/terms.c b/src/term.c
similarity index 99%
rename from src/terms.c
rename to src/term.c
index 8d79e2b..656ed55 100644
--- a/src/terms.c
+++ b/src/term.c
@@ -10,11 +10,11 @@
  * pointer comparison, which is what we want. However, for comparison of terms
  */
 
-#include <strings.h>
+#include <string.h>
 #include <stdlib.h>
 #include <stdio.h>
 #include <limits.h>
-#include "terms.h"
+#include "term.h"
 #include "debug.h"
 #include "memory.h"
 #include "ctype.h"
diff --git a/src/terms.h b/src/term.h
similarity index 99%
rename from src/terms.h
rename to src/term.h
index b965785..faf5834 100644
--- a/src/terms.h
+++ b/src/term.h
@@ -1,7 +1,7 @@
 #ifndef TERMS
 #define TERMS
 
-#include "symbols.h"
+#include "symbol.h"
 
 #define	GLOBAL	 1
 #define VARIABLE 2
diff --git a/src/termlists.c b/src/termlist.c
similarity index 99%
rename from src/termlists.c
rename to src/termlist.c
index d5900f1..c987ead 100644
--- a/src/termlists.c
+++ b/src/termlist.c
@@ -1,6 +1,6 @@
 #include <stdlib.h>
 #include <stdio.h>
-#include "termlists.h"
+#include "termlist.h"
 #include "debug.h"
 #include "memory.h"
 
diff --git a/src/termlists.h b/src/termlist.h
similarity index 99%
rename from src/termlists.h
rename to src/termlist.h
index e22e2ff..a1958d8 100644
--- a/src/termlists.h
+++ b/src/termlist.h
@@ -1,7 +1,7 @@
 #ifndef TERMLISTS
 #define TERMLISTS
 
-#include "terms.h"
+#include "term.h"
 
 //! The list container for the term type.
 /**
diff --git a/src/temmap.c b/src/termmap.c
similarity index 100%
rename from src/temmap.c
rename to src/termmap.c
diff --git a/src/temmap.h b/src/termmap.h
similarity index 100%
rename from src/temmap.h
rename to src/termmap.h
diff --git a/src/termmaps.c b/src/termmaps.c
deleted file mode 100644
index 4d4d8d7..0000000
--- a/src/termmaps.c
+++ /dev/null
@@ -1,123 +0,0 @@
-#include <stdlib.h>
-#include <stdio.h>
-#include "termmaps.h"
-#include "debug.h"
-#include "memory.h"
-
-//! Open termmaps code.
-void
-termmapsInit (void)
-{
-  return;
-}
-
-//! Close termmaps code.
-void
-termmapsDone (void)
-{
-  return;
-}
-
-//! Allocate memory for a termmap node.
-/**
- *@return A pointer to uninitialised memory of the size of a termmap node.
- */
-Termmap
-makeTermmap (void)
-{
-  /* inline candidate */
-  return (Termmap) memAlloc (sizeof (struct termmap));
-}
-
-//! Get function result
-/**
- *@return Yields f(x), or -1 when it is not present.
- */
-int
-termmapGet (Termmap f, const Term x)
-{
-  while (f != NULL)
-    {
-      if (isTermEqual (x, f->term))
-	  return f->result;
-      f = f->next;
-    }
-  return -1;
-}
-
-//! Add a value to a function.
-/**
- *@return Adds f(x)=y to an existing function f. If f is NULL, a function is created. If x is already in the domain, the value is replaced.
- */
-Termmap
-termmapSet (const Termmap f, const Term x, const int y)
-{
-  Termmap fscan;
-
-  //! Determine whether term already occurs
-  fscan = f;
-  while (fscan != NULL)
-    {
-      if (isTermEqual (x, fscan->term))
-	{
-	  //! Is the result correct already?
-	  if (fscan->result != y)
-	      fscan->result = y;
-          return f;
-	}
-      fscan = fscan->next;
-    }
-  //! Not occurred yet, make new node
-  fscan = makeTermmap ();
-  fscan->term = x;
-  fscan->result = y;
-  fscan->next = f;
-  return fscan;
-}
-
-//! Duplicate a function
-Termmap
-termmapDuplicate (const Termmap f)
-{
-  if (f != NULL)
-    {
-      Termmap g;
-
-      g = makeTermmap ();
-      g->term = f->term;
-      g->result = f->result;
-      g->next = termmapDuplicate (f->next);
-      return g;
-    }
-  else
-    {
-      return NULL;
-    }
-}
-
-//! Delete a function
-void
-termmapDelete (const Termmap f)
-{
-  if (f != NULL)
-    {
-      termmapDelete (f->next);
-      memFree (f, sizeof (struct termmap));
-    }
-}
-
-//! Print a function
-void termmapPrint (Termmap f)
-{
-  if (f != NULL)
-    {
-      printf ("\"");
-      termPrint (f->term);
-      printf ("\" -> %i", f->result);
-      if (f->next != NULL)
-	{
-	  printf (", ");
-	  termmapPrint (f->next);
-	}
-    }
-}
diff --git a/src/termmaps.h b/src/termmaps.h
deleted file mode 100644
index 8138abf..0000000
--- a/src/termmaps.h
+++ /dev/null
@@ -1,31 +0,0 @@
-#ifndef TERMMAPS
-#define TERMMAPS
-
-#include "terms.h"
-
-//! The function container for the term to integer function type.
-/**
- *\sa term
- */
-struct termmap
-{
-  //! The term element for this node.
-  Term term;
-  //! Next node pointer or NULL for the last element of the function.
-  struct termmap *next;
-  //! Function result
-  int result;
-};
-
-//! Shorthand for termmap pointers.
-typedef struct termmap *Termmap;
-
-void termmapsInit (void);
-void termmapsDone (void);
-int termmapGet (Termmap f, const Term x);
-Termmap termmapSet (const Termmap f, const Term x, const int y);
-Termmap termmapDuplicate (const Termmap f);
-void termmapDelete (const Termmap f);
-void termmapPrint (Termmap f);
-
-#endif
diff --git a/src/tracebuf.h b/src/tracebuf.h
index 79a42fe..435634d 100644
--- a/src/tracebuf.h
+++ b/src/tracebuf.h
@@ -1,8 +1,8 @@
 #ifndef TRACEBUF
 #define TRACEBUF
 
-#include "terms.h"
-#include "termlists.h"
+#include "term.h"
+#include "termlist.h"
 #include "knowledge.h"
 #include "system.h"