diff --git a/src/type.c b/src/type.c
index ebfa10a..9212ec5 100644
--- a/src/type.c
+++ b/src/type.c
@@ -14,6 +14,7 @@
 #include "specialterm.h"
 
 extern Protocol INTRUDER;
+extern Termlist TERMLISTERROR;
 
 //! Report a bad substitution, if needed
 void
@@ -42,6 +43,44 @@ reportBadSubst (const Term tvar, const Term tsubst)
 #endif
 }
 
+//! Say whether a typelist is 'generic' or should be taken per item.
+int
+isTypelistGeneric (const Termlist typelist)
+{
+  if (typelist == NULL)
+    {
+      return 1;
+    }
+  else
+    {
+      return inTermlist (typelist, TERM_Ticket);
+    }
+}
+
+//! Check whether a single type constant matches a typelist
+/**
+ * Understands semantics of NULL and TERM_Ticket
+ */
+int
+matchSingleType (Termlist typelist, Term type)
+{
+  if (typelist == TERMLISTERROR)
+    {
+      return 0;
+    }
+  else
+    {
+      if (isTypelistGeneric (typelist))
+	{
+	  return 1;
+	}
+      else
+	{
+	  return inTermlist (typelist, type);
+	}
+    }
+}
+
 //! Check whether a single variable term is instantiated correctly.
 /**
  * Check whether a single variable term is instantiated correctly in this
@@ -59,47 +98,42 @@ checkTypeTerm (const int mgumode, const Term tvar)
       // Non-instantiated terms are fine.
       if (tvar->subst != NULL)
 	{
-	  // NULL type is always fine
-	  if (tvar->stype != NULL)
+	  if (!isTypelistGeneric (tvar->stype))
 	    {
-	      // Tickets are always fine too
-	      if (!inTermlist (tvar->stype, TERM_Ticket))
-		{
-		  // So there is a specific (non-ticket) type, and the var is instantiated, match mode 0 or 1
-		  // Is it really a leaf?
-		  Term tsubst;
+	      // So there is a specific (non-ticket) type, and the var is instantiated, match mode 0 or 1
+	      // Is it really a leaf?
+	      Term tsubst;
 
-		  tsubst = deVar (tvar);
-		  if (!realTermLeaf (tsubst))
+	      tsubst = deVar (tvar);
+	      if (!realTermLeaf (tsubst))
+		{
+		  // Then it's definitively false
+		  reportBadSubst (tvar, tsubst);
+		  return false;
+		}
+	      else
+		{
+		  // It is a leaf
+		  if (mgumode == 0)
 		    {
-		      // Then it's definitively false
+		      /* Types must match exactly. Thus, one of the variable type should match a type of the constant.
+		       */
+		      Termlist tl;
+
+		      tl = tvar->stype;
+		      while (tl != NULL)
+			{
+			  if (inTermlist (tsubst->stype, tl->term))
+			    {
+			      // One type matches
+			      return true;
+			    }
+			  tl = tl->next;
+			}
+		      // No type matches.
 		      reportBadSubst (tvar, tsubst);
 		      return false;
 		    }
-		  else
-		    {
-		      // It is a leaf
-		      if (mgumode == 0)
-			{
-			  /* Types must match exactly. Thus, one of the variable type should match a type of the constant.
-			   */
-			  Termlist tl;
-
-			  tl = tvar->stype;
-			  while (tl != NULL)
-			    {
-			      if (inTermlist (tsubst->stype, tl->term))
-				{
-				  // One type matches
-				  return true;
-				}
-			      tl = tl->next;
-			    }
-			  // No type matches.
-			  reportBadSubst (tvar, tsubst);
-			  return false;
-			}
-		    }
 		}
 	    }
 	}
@@ -141,3 +175,272 @@ checkTypeLocals (const System sys)
     }
   return true;
 }
+
+//! Check whether a typelist is a strict agent type list
+int
+isAgentType (Termlist typelist)
+{
+  return (termlistLength (typelist) == 1 &&
+	  inTermlist (typelist, TERM_Agent));
+}
+
+//! Helper function to determine whether a list is compatible with an agent var.
+int
+agentCompatible (Termlist tl)
+{
+  if (isTypelistGeneric (tl))
+    {
+      return 1;
+    }
+  else
+    {
+      return inTermlist (tl, TERM_Agent);
+    }
+}
+
+//! Check whether two type lists are compatible for variables
+/**
+ * Depends on some input:
+ *
+ * mgumode	type of matching
+ * agentcheck	true if agent type is always restrictive
+ *
+ * returns the new type list (needs to be deleted!) or TERMLISTERROR (should
+ * not be deleted!)
+ */
+Termlist
+typelistConjunct (Termlist typelist1, Termlist typelist2, const int mgumode,
+		  const int agentcheck)
+{
+  if (typelist1 != TERMLISTERROR && typelist2 != TERMLISTERROR)
+    {
+
+      /* In the restricted agent case, we check whether agent list occurs in
+       * either set. If so, the result can only be an agent-restrictive list.
+       */
+
+      if (agentcheck)
+	{
+	  if (isAgentType (typelist1) || isAgentType (typelist2))
+	    {
+	      /* Now, the result must surely accept agents. Thus, it must be
+	       * NULL or accept agents.
+	       */
+
+	      if (!
+		  (agentCompatible (typelist1)
+		   && agentCompatible (typelist2)))
+		{
+		  // Not good: one of them cannot
+		  return TERMLISTERROR;
+		}
+	      else
+		{
+		  // Good: but because an agent is involved, the type reduces to the simple Agent type only.
+		  return termlistAdd (NULL, TERM_Agent);
+		}
+	    }
+	  else
+	    {
+	      /* Not the simple agent variable case. Now other things come in to play.
+	       */
+	      if (mgumode == 0)
+		{
+		  /*
+		   * Strict match: (-m0) conjunct of the types must be non-empty.
+		   */
+
+		  // Generic exceptions
+		  if (isTypelistGeneric (typelist1))
+		    {
+		      // Copy for later deletion
+		      return termlistShallow (typelist2);
+		    }
+		  else
+		    {
+		      if (isTypelistGeneric (typelist2))
+			{
+			  // Copy for later deletion
+			  return termlistShallow (typelist1);
+			}
+		      else
+			{
+			  /* Apparently neither is generic, and we can take the real conjunct.
+			   * However, this conjunct must not be empty (because that implies that the types cannot match).
+			   */
+			  Termlist conjunct;
+
+			  conjunct = termlistConjunct (typelist1, typelist2);
+			  if (conjunct == NULL)
+			    {
+			      // Empty, and thus the variables cannot be instantiated without causing a type flaw.
+			      return TERMLISTERROR;
+			    }
+			  else
+			    {
+			      // Non-empty, which is good in this case.
+			      return conjunct;
+			    }
+			}
+		    }
+		}
+	      else
+		{
+		  /*
+		   * Not so strict: (-m1 or -m2)
+		   *
+		   * Because the variable is not bound, there is certainly no
+		   * binding yet to tuples or crypted terms, and thus any
+		   * typing will do.
+		   */
+		  return NULL;
+		}
+	    }
+	}
+    }
+  return TERMLISTERROR;
+}
+
+//! Check a single ground variable
+/**
+ * Check whether all variables that map to this one have a possible valid substitution
+ */
+int
+checkGroundVariable (const System sys, const Term groundvar)
+{
+  int allvalid;
+
+  allvalid = 1;
+  if (realTermVariable (groundvar))
+    {
+      Termlist tl;
+      Termlist typelist;
+
+      // Check
+      typelist = termlistShallow (groundvar->stype);
+      tl = sys->variables;
+      while (allvalid == 1 && tl != NULL)
+	{
+	  Term term;
+
+	  term = tl->term;
+
+	  // Not actually the same, of course
+	  if (term != groundvar)
+	    {
+	      // Does this term map to the same variable?
+	      if (isTermEqual (term, groundvar))
+		{
+		  Termlist tlprev;
+
+		  // Maps to same ground term
+		  // Take conjunct
+		  tlprev = typelist;
+		  typelist =
+		    typelistConjunct (tlprev, term->stype, switches.match,
+				      switches.agentTypecheck);
+		  termlistDelete (tlprev);
+
+		  if (typelist == TERMLISTERROR)
+		    {
+		      // And this is not valid...
+		      allvalid = 0;
+		    }
+		}
+	    }
+	  tl = tl->next;
+	}
+      if (typelist != TERMLISTERROR)
+	{
+	  termlistDelete (typelist);
+	}
+    }
+  return allvalid;
+}
+
+
+//! Global check of the system, for all variables.
+/**
+ * Returns true if all variables are okay.
+ *
+ * This version checks all substitutions, and thus takes over all the functions
+ * that are now in mgu.c. However, we have left them in for speed purposes,
+ * because pruning early is good.
+ */
+int
+checkAllSubstitutions (const System sys)
+{
+  int allvalid;
+  Termlist groundvars;
+  Termlist tl;
+
+  /* We scan all unbound variables for so called 'ground variables', which are
+   * the root of a substitution tree. Such variables are checked for
+   * satisfyability, i.e. the conjunction of their type lists must not be
+   * empty.
+   *
+   * At the same time, we check also bound variables for their mappings.
+   */
+  groundvars = NULL;
+  allvalid = 1;
+  tl = sys->variables;
+  while ((allvalid == 1) && (tl != NULL))
+    {
+      Term tvar;
+
+      tvar = tl->term;
+      if (realTermVariable (tvar))
+	{
+	  Term tsubst;
+
+	  tsubst = deVar (tvar);
+
+	  if (tvar != tsubst)
+	    {
+	      // Substitution going on, check
+
+	      if (realTermVariable (tsubst))
+		{
+		  /* Variable -> Variable (unbound)
+		   *
+		   * Check whether we already scanned for this one, because we
+		   * don't want to scan for this ground variable more than once.
+		   */
+		  if (!inTermlist (groundvars, tsubst))
+		    {
+		      /* Not done before, add now.
+		       */
+		      groundvars = termlistAdd (groundvars, tsubst);
+
+		      /* Check whether there exists a valid substitution for
+		       * everything mapping to this ground variable.
+		       */
+		      allvalid = allvalid
+			&& checkGroundVariable (sys, tsubst);
+		    }
+		}
+	      else
+		{
+		  /* Variable -> term (bound)
+		   */
+
+		  if (switches.agentTypecheck && isAgentType (tvar->stype))
+		    {
+		      // *Must* include agent type, regardless of match
+		      allvalid = allvalid && agentCompatible (tsubst->stype);
+		    }
+		  else
+		    {
+		      // Consider match
+		      allvalid = allvalid
+			&& checkTypeTerm (switches.match, tvar);
+		    }
+		}
+	    }
+	}
+      tl = tl->next;
+    }
+
+  termlistDelete (groundvars);
+  return allvalid;
+}
diff --git a/src/type.h b/src/type.h
index 4681c8b..91a5929 100644
--- a/src/type.h
+++ b/src/type.h
@@ -7,5 +7,8 @@
 int checkTypeTerm (const int mgumode, const Term t);
 int checkTypeTermlist (const int mgumode, Termlist tl);
 int checkTypeLocals (const System sys);
+Termlist typelistConjunct (Termlist typelist1, Termlist Typelist2);
+int checkAllSubstitutions (const System sys);
+int isAgentType (Termlist typelist);
 
 #endif