diff --git a/src/binding.c b/src/binding.c
index da64e1c..cbe5294 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -300,6 +300,28 @@ goal_remove_last (int n)
     }
 }
 
+//! Get index of run
+int
+get_index (const int run, const Term label)
+{
+  Roledef rd;
+  int i;
+
+  i = 0;
+  rd = sys->runs[run].start;
+  while (rd != NULL && !isTermEqual (rd->label, label))
+    {
+      rd = rd->next;
+      i++;
+    }
+#ifdef DEBUG
+  if (rd == NULL)
+    error
+      ("Could not locate send or recv for label, after niagree holds, to test for order.");
+#endif
+  return i;
+}
+
 //! Determine whether some label set is ordered w.r.t. send/recv order.
 /**
  * Assumes all these labels exist in the system, within length etc, and that the run mappings are valid.
@@ -312,34 +334,16 @@ labels_ordered (Termmap runs, Termlist labels)
       // Given this label, and the mapping of runs, we want to know if the order is okay. Thus, we need to know sendrole and recvrole
       Labelinfo linfo;
       int send_run, send_ev, recv_run, recv_ev;
+      Term label;
 
-      int get_index (const int run)
-      {
-	Roledef rd;
-	int i;
-
-	i = 0;
-	rd = sys->runs[run].start;
-	while (rd != NULL && !isTermEqual (rd->label, labels->term))
-	  {
-	    rd = rd->next;
-	    i++;
-	  }
-#ifdef DEBUG
-	if (rd == NULL)
-	  error
-	    ("Could not locate send or recv for label, after niagree holds, to test for order.");
-#endif
-	return i;
-      }
-
-      linfo = label_find (sys->labellist, labels->term);
+      label = labels->term;
+      linfo = label_find (sys->labellist, label);
       if (!linfo->ignore)
 	{
 	  send_run = termmapGet (runs, linfo->sendrole);
 	  recv_run = termmapGet (runs, linfo->recvrole);
-	  send_ev = get_index (send_run);
-	  recv_ev = get_index (recv_run);
+	  send_ev = get_index (send_run, label);
+	  recv_ev = get_index (recv_run, label);
 	  if (!isDependEvent (send_run, send_ev, recv_run, recv_ev))
 	    {
 	      // Not ordered; false
diff --git a/src/claim.c b/src/claim.c
index e42fc00..644672d 100644
--- a/src/claim.c
+++ b/src/claim.c
@@ -514,7 +514,59 @@ check_claim_niagree (const System sys, const int i)
   return result;
 }
 
+//! Get label event
+Roledef
+get_label_event (const System sys, const Labelinfo linfo, const Term role,
+		 const Term label, const Termmap runs)
+{
+  Roledef rd, rd_res;
+  int i;
+  int run;
 
+  run = termmapGet (runs, role);
+  if (run != -1)
+    {
+#ifdef DEBUG
+      if (run < 0 || run >= sys->maxruns)
+	{
+	  globalError++;
+	  eprintf ("Run mapping %i out of bounds for role ", run);
+	  termPrint (role);
+	  eprintf (" and label ");
+	  termPrint (label);
+	  eprintf ("\n");
+	  eprintf ("This label has sendrole ");
+	  termPrint (linfo->sendrole);
+	  eprintf (" and recvrole ");
+	  termPrint (linfo->recvrole);
+	  eprintf ("\n");
+	  globalError--;
+	  error ("Run mapping is out of bounds.");
+	}
+#endif
+      rd = sys->runs[run].start;
+      rd_res = NULL;
+      i = 0;
+      while (i < sys->runs[run].step && rd != NULL)
+	{
+	  if (isTermEqual (rd->label, label))
+	    {
+	      rd_res = rd;
+	      rd = NULL;
+	    }
+	  else
+	    {
+	      rd = rd->next;
+	    }
+	  i++;
+	}
+      return rd_res;
+    }
+  else
+    {
+      return NULL;
+    }
+}
 
 //! Check generic agree claim for a given set of runs, arachne style
 int
@@ -541,63 +593,14 @@ arachne_runs_agree (const System sys, const Claimlist cl, const Termmap runs)
       Roledef rd_send, rd_recv;
       Labelinfo linfo;
 
-      Roledef get_label_event (const Term role, const Term label)
-      {
-	Roledef rd, rd_res;
-	int i;
-	int run;
-
-	run = termmapGet (runs, role);
-	if (run != -1)
-	  {
-#ifdef DEBUG
-	    if (run < 0 || run >= sys->maxruns)
-	      {
-		globalError++;
-		eprintf ("Run mapping %i out of bounds for role ", run);
-		termPrint (role);
-		eprintf (" and label ");
-		termPrint (label);
-		eprintf ("\n");
-		eprintf ("This label has sendrole ");
-		termPrint (linfo->sendrole);
-		eprintf (" and recvrole ");
-		termPrint (linfo->recvrole);
-		eprintf ("\n");
-		globalError--;
-		error ("Run mapping is out of bounds.");
-	      }
-#endif
-	    rd = sys->runs[run].start;
-	    rd_res = NULL;
-	    i = 0;
-	    while (i < sys->runs[run].step && rd != NULL)
-	      {
-		if (isTermEqual (rd->label, label))
-		  {
-		    rd_res = rd;
-		    rd = NULL;
-		  }
-		else
-		  {
-		    rd = rd->next;
-		  }
-		i++;
-	      }
-	    return rd_res;
-	  }
-	else
-	  {
-	    return NULL;
-	  }
-      }
-
       // Main
       linfo = label_find (sys->labellist, labels->term);
       if (!linfo->ignore)
 	{
-	  rd_send = get_label_event (linfo->sendrole, labels->term);
-	  rd_recv = get_label_event (linfo->recvrole, labels->term);
+	  rd_send =
+	    get_label_event (sys, linfo, linfo->sendrole, labels->term, runs);
+	  rd_recv =
+	    get_label_event (sys, linfo, linfo->recvrole, labels->term, runs);
 
 	  if (rd_send == NULL || rd_recv == NULL)
 	    {
diff --git a/src/compiler.c b/src/compiler.c
index d4de5b3..a74bc4c 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -1183,31 +1183,33 @@ normalDeclaration (Tac tc)
   return 1;
 }
 
+  /* first: secrecy claims for all locally declared things */
+void
+addSecrecyList (const System sys, const Protocol protocol, const Role role,
+		Termlist tl)
+{
+  while (tl != NULL)
+    {
+      Term t;
+
+      t = deVar (tl->term);
+      if (realTermLeaf (t))
+	{
+	  // Add a secrecy claim
+	  claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1);
+	}
+      tl = tl->next;
+    }
+}
+
 //! Add all sorts of claims to this role
 void
 claimAddAll (const System sys, const Protocol protocol, const Role role)
 {
-  /* first: secrecy claims for all locally declared things */
-  void addSecrecyList (Termlist tl)
-  {
-    while (tl != NULL)
-      {
-	Term t;
-
-	t = deVar (tl->term);
-	if (realTermLeaf (t))
-	  {
-	    // Add a secrecy claim
-	    claimCreate (sys, protocol, role, CLAIM_Secret, NULL, t, -1);
-	  }
-	tl = tl->next;
-      }
-  }
-
   if (!isHelperProtocol (protocol))
     {
-      addSecrecyList (role->declaredconsts);
-      addSecrecyList (role->declaredvars);
+      addSecrecyList (sys, protocol, role, role->declaredconsts);
+      addSecrecyList (sys, protocol, role, role->declaredvars);
 
       /* full non-injective agreement and ni-synch */
       claimCreate (sys, protocol, role, CLAIM_Alive, NULL, NULL, -1);
@@ -1699,6 +1701,26 @@ compute_label_roles (Termlist labels)
   return roles;
 }
 
+		      // This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements.
+int
+roles_test (const Termlist roles_ordered, const Termlist roles_remaining,
+	    const Term connectedrole, const Term newrole)
+{
+  if (inTermlist (roles_ordered, connectedrole) &&
+      inTermlist (roles_remaining, newrole))
+    {
+#ifdef DEBUG
+      if (DEBUGL (4))
+	{
+	  eprintf (" ");
+	  termPrint (newrole);
+	}
+#endif
+      return true;
+    }
+  return false;
+}
+
 //! Order the label roles for a given claim
 void
 order_label_roles (const Claimlist cl)
@@ -1749,30 +1771,28 @@ order_label_roles (const Claimlist cl)
 		    {
 		      // If it's not the same protocol, the labels can't match
 
-		      // This function checks whether the newrole can connect to the connectedrole, and whether they fulfil their requirements.
-		      void roles_test (const Term connectedrole,
-				       const Term newrole)
-		      {
-			if (inTermlist (roles_ordered, connectedrole) &&
-			    inTermlist (roles_remaining, newrole))
-			  {
-#ifdef DEBUG
-			    if (DEBUGL (4))
-			      {
-				eprintf (" ");
-				termPrint (newrole);
-			      }
-#endif
-			    roles_ordered =
-			      termlistAppend (roles_ordered, newrole);
-			    roles_remaining =
-			      termlistDelTerm (termlistFind
-					       (roles_remaining, newrole));
-			  }
-		      }
-
-		      roles_test (linfo->sendrole, linfo->recvrole);
-		      roles_test (linfo->recvrole, linfo->sendrole);
+		      if (roles_test
+			  (roles_ordered, roles_remaining, linfo->sendrole,
+			   linfo->recvrole))
+			{
+			  roles_ordered =
+			    termlistAppend (roles_ordered, linfo->recvrole);
+			  roles_remaining =
+			    termlistDelTerm (termlistFind
+					     (roles_remaining,
+					      linfo->recvrole));
+			}
+		      if (roles_test
+			  (roles_ordered, roles_remaining, linfo->recvrole,
+			   linfo->sendrole))
+			{
+			  roles_ordered =
+			    termlistAppend (roles_ordered, linfo->sendrole);
+			  roles_remaining =
+			    termlistDelTerm (termlistFind
+					     (roles_remaining,
+					      linfo->sendrole));
+			}
 		    }
 		}
 	    }
@@ -1788,6 +1808,84 @@ order_label_roles (const Claimlist cl)
 #endif
 }
 
+  // Assist: compute m_index from role, lev
+int
+m_index (const System sys, const int r, const int lev)
+{
+  return r * sys->roleeventmax + lev;
+}
+
+  // Assist: yield roledef from r, lev
+Roledef
+roledef_re (const System sys, int r, int lev)
+{
+  Protocol pr;
+  Role ro;
+  Roledef rd;
+
+  pr = sys->protocols;
+  ro = pr->roles;
+  while (r > 0 && ro != NULL)
+    {
+      ro = ro->next;
+      if (ro == NULL)
+	{
+	  pr = pr->next;
+	  if (pr != NULL)
+	    {
+	      ro = pr->roles;
+	    }
+	  else
+	    {
+	      ro = NULL;
+	    }
+	}
+      r--;
+    }
+  if (ro != NULL)
+    {
+      rd = ro->roledef;
+      while (lev > 0 && rd != NULL)
+	{
+	  rd = rd->next;
+	  lev--;
+	}
+      return rd;
+    }
+  else
+    {
+      return NULL;
+    }
+}
+
+  //! Assist: print matrix
+void
+show_matrix (const System sys, const int rowsize, const unsigned int *prec)
+{
+  int r1, r2, ev1, ev2;
+
+  for (r1 = 0; r1 < sys->rolecount; r1++)
+    {
+      for (ev1 = 0; ev1 < sys->roleeventmax; ev1++)
+	{
+	  eprintf ("prec %i,%i:  ", r1, ev1);
+	  for (r2 = 0; r2 < sys->rolecount; r2++)
+	    {
+	      for (ev2 = 0; ev2 < sys->roleeventmax; ev2++)
+		{
+		  eprintf ("%i ",
+			   BIT (prec + rowsize * m_index (sys, r2, ev2),
+				m_index (sys, r1, ev1)));
+		}
+	      eprintf (" ");
+	    }
+	  eprintf ("\n");
+	}
+      eprintf ("\n");
+    }
+  eprintf ("\n");
+}
+
 //! Compute prec() sets for each claim.
 /**
  * Generates two auxiliary structures. First, a table that contains
@@ -1808,89 +1906,6 @@ compute_prec_sets (const System sys)
   int r1, r2, ev1, ev2;		// some counters
   Claimlist cl;
 
-  // Assist: compute index from role, lev
-  int index (int r, int lev)
-  {
-    return r * sys->roleeventmax + lev;
-  }
-
-  // Assist: yield roledef from r, lev
-  Roledef roledef_re (int r, int lev)
-  {
-    Protocol pr;
-    Role ro;
-    Roledef rd;
-
-    pr = sys->protocols;
-    ro = pr->roles;
-    while (r > 0 && ro != NULL)
-      {
-	ro = ro->next;
-	if (ro == NULL)
-	  {
-	    pr = pr->next;
-	    if (pr != NULL)
-	      {
-		ro = pr->roles;
-	      }
-	    else
-	      {
-		ro = NULL;
-	      }
-	  }
-	r--;
-      }
-    if (ro != NULL)
-      {
-	rd = ro->roledef;
-	while (lev > 0 && rd != NULL)
-	  {
-	    rd = rd->next;
-	    lev--;
-	  }
-	return rd;
-      }
-    else
-      {
-	return NULL;
-      }
-  }
-
-  // Assist: print matrix
-  void show_matrix (void)
-  {
-    int r1, r2, ev1, ev2;
-
-    r1 = 0;
-    while (r1 < sys->rolecount)
-      {
-	ev1 = 0;
-	while (ev1 < sys->roleeventmax)
-	  {
-	    eprintf ("prec %i,%i:  ", r1, ev1);
-	    r2 = 0;
-	    while (r2 < sys->rolecount)
-	      {
-		ev2 = 0;
-		while (ev2 < sys->roleeventmax)
-		  {
-		    eprintf ("%i ",
-			     BIT (prec + rowsize * index (r2, ev2),
-				  index (r1, ev1)));
-		    ev2++;
-		  }
-		eprintf (" ");
-		r2++;
-	      }
-	    eprintf ("\n");
-	    ev1++;
-	  }
-	eprintf ("\n");
-	r1++;
-      }
-    eprintf ("\n");
-  }
-
   /*
    * Phase 1: Allocate structures and map to labels
    */
@@ -1907,10 +1922,10 @@ compute_prec_sets (const System sys)
       Roledef rd;
 
       ev1 = 0;
-      rd = roledef_re (r1, ev1);
+      rd = roledef_re (sys, r1, ev1);
       while (rd != NULL)
 	{
-	  eventlabels[index (r1, ev1)] = rd->label;
+	  eventlabels[m_index (sys, r1, ev1)] = rd->label;
 	  //termPrint (rd->label);
 	  //eprintf ("\t");
 	  ev1++;
@@ -1918,7 +1933,7 @@ compute_prec_sets (const System sys)
 	}
       while (ev1 < sys->roleeventmax)
 	{
-	  eventlabels[index (r1, ev1)] = NULL;
+	  eventlabels[m_index (sys, r1, ev1)] = NULL;
 	  ev1++;
 	}
       //eprintf ("\n");
@@ -1931,7 +1946,8 @@ compute_prec_sets (const System sys)
       ev1 = 1;
       while (ev1 < (sys->roleeventmax))
 	{
-	  SETBIT (prec + rowsize * index (r1, ev1 - 1), index (r1, ev1));
+	  SETBIT (prec + rowsize * m_index (sys, r1, ev1 - 1),
+		  m_index (sys, r1, ev1));
 	  ev1++;
 	}
       r1++;
@@ -1945,7 +1961,7 @@ compute_prec_sets (const System sys)
 	{
 	  Roledef rd1;
 
-	  rd1 = roledef_re (r1, ev1);
+	  rd1 = roledef_re (sys, r1, ev1);
 	  if (rd1 != NULL && rd1->type == SEND)
 	    {
 	      r2 = 0;
@@ -1956,12 +1972,12 @@ compute_prec_sets (const System sys)
 		    {
 		      Roledef rd2;
 
-		      rd2 = roledef_re (r2, ev2);
+		      rd2 = roledef_re (sys, r2, ev2);
 		      if (rd2 != NULL && rd2->type == RECV
 			  && isTermEqual (rd1->label, rd2->label))
 			{
-			  SETBIT (prec + rowsize * index (r1, ev1),
-				  index (r2, ev2));
+			  SETBIT (prec + rowsize * m_index (sys, r1, ev1),
+				  m_index (sys, r2, ev2));
 			}
 		      ev2++;
 		    }
@@ -1976,7 +1992,7 @@ compute_prec_sets (const System sys)
 #ifdef DEBUG
   if (DEBUGL (5))
     {
-      show_matrix ();
+      show_matrix (sys, rowsize, prec);
     }
 #endif
 
@@ -1988,7 +2004,7 @@ compute_prec_sets (const System sys)
 #ifdef DEBUG
   if (DEBUGL (5))
     {
-      show_matrix ();
+      show_matrix (sys, rowsize, prec);
     }
 #endif
 
@@ -2016,14 +2032,14 @@ compute_prec_sets (const System sys)
 	    }
 	}
       while (r1 < sys->rolecount
-	     && !isTermEqual (label, eventlabels[index (r1, ev1)]));
+	     && !isTermEqual (label, eventlabels[m_index (sys, r1, ev1)]));
 
       if (r1 == sys->rolecount)
 	{
 	  error
 	    ("Prec() setup: Could not find the event corresponding to a claim label.");
 	}
-      rd = roledef_re (r1, ev1);
+      rd = roledef_re (sys, r1, ev1);
       if (rd->type != CLAIM)
 	{
 	  error
@@ -2039,15 +2055,15 @@ compute_prec_sets (const System sys)
        * Now we compute the preceding label set
        */
       cl->prec = NULL;		// clear first
-      claim_index = index (r1, ev1);
+      claim_index = m_index (sys, r1, ev1);
       r2 = 0;
       while (r2 < sys->rolecount)
 	{
 	  ev2 = 0;
-	  rd = roledef_re (r2, ev2);
+	  rd = roledef_re (sys, r2, ev2);
 	  while (rd != NULL)
 	    {
-	      if (BIT (prec + rowsize * index (r2, ev2), claim_index))
+	      if (BIT (prec + rowsize * m_index (sys, r2, ev2), claim_index))
 		{
 		  // This event precedes the claim
 
@@ -2118,12 +2134,12 @@ compute_prec_sets (const System sys)
 		    {
 		      // if this event preceds the claim, replace the label term
 		      if (BIT
-			  (prec + rowsize * index (r_scan, ev_scan),
+			  (prec + rowsize * m_index (sys, r_scan, ev_scan),
 			   claim_index))
 			{
 			  Roledef rd;
 
-			  rd = roledef_re (r_scan, ev_scan);
+			  rd = roledef_re (sys, r_scan, ev_scan);
 			  if (rd->label != NULL)
 			    {
 			      t_buf = rd->label;
diff --git a/src/dotout.c b/src/dotout.c
index 1f9cd76..5259fea 100644
--- a/src/dotout.c
+++ b/src/dotout.c
@@ -263,30 +263,31 @@ redirNode (const System sys, Binding b)
   node (sys, b->run_to, b->ev_to);
 }
 
+void
+optlabel (const Roledef rd)
+{
+  Term label;
+
+  label = rd->label;
+  if (label != NULL)
+    {
+      if (realTermTuple (label))
+	{
+	  label = TermOp2 (label);
+	}
+      eprintf ("_");
+      termPrintRemap (label);
+    }
+}
+
 //! Roledef draw
 void
 roledefDraw (Roledef rd)
 {
-  void optlabel (void)
-  {
-    Term label;
-
-    label = rd->label;
-    if (label != NULL)
-      {
-	if (realTermTuple (label))
-	  {
-	    label = TermOp2 (label);
-	  }
-	eprintf ("_");
-	termPrintRemap (label);
-      }
-  }
-
   if (rd->type == RECV)
     {
       eprintf ("recv");
-      optlabel ();
+      optlabel (rd);
       eprintf (" from ");
       termPrintRemap (rd->from);
       eprintf ("\\n");
@@ -295,7 +296,7 @@ roledefDraw (Roledef rd)
   if (rd->type == SEND)
     {
       eprintf ("send");
-      optlabel ();
+      optlabel (rd);
       eprintf (" to ");
       termPrintRemap (rd->to);
       eprintf ("\\n");
@@ -304,7 +305,7 @@ roledefDraw (Roledef rd)
   if (rd->type == CLAIM)
     {
       eprintf ("claim");
-      optlabel ();
+      optlabel (rd);
       eprintf ("\\n");
       termPrintRemap (rd->to);
       if (rd->message != NULL)
@@ -348,25 +349,26 @@ hlsValue (double n1, double n2, double hue)
     return n1;
 }
 
+int
+bytedouble (double d)
+{
+  double x;
+
+  x = 255.0 * d;
+  if (x <= 0)
+    return 0;
+  else if (x >= 255.0)
+    return 255;
+  else
+    return (int) x;
+}
+
 //! hls to rgb conversion
 void
 hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
 {
   double m1, m2;
 
-  int bytedouble (double d)
-  {
-    double x;
-
-    x = 255.0 * d;
-    if (x <= 0)
-      return 0;
-    else if (x >= 255.0)
-      return 255;
-    else
-      return (int) x;
-  }
-
   while (h >= 360.0)
     h -= 360.0;
   while (h < 0)
@@ -385,6 +387,12 @@ hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
     }
 }
 
+double
+closer (double l, double factor)
+{
+  return l + ((1.0 - l) * factor);
+}
+
 //! hls to rgb conversion
 /**
  * Secretly takes the monochrome switch into account
@@ -392,11 +400,6 @@ hlsrgbreal (int *r, int *g, int *b, double h, double l, double s)
 void
 hlsrgb (int *r, int *g, int *b, double h, double l, double s)
 {
-  double closer (double l, double factor)
-  {
-    return l + ((1.0 - l) * factor);
-  }
-
   if (switches.monochrome)
     {
       // No colors
@@ -432,6 +435,14 @@ printColor (double h, double l, double s)
   eprintf ("#%02x%02x%02x", r, g, b);
 }
 
+  // help function: contract roleoffset, roledelta with a factor (<= 1.0)
+void
+contract (double roledelta, double roleoffset, double factor)
+{
+  roledelta = roledelta * factor;
+  roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0);
+}
+
 
 //! Set local buffer with the correct color for this run.
 /**
@@ -453,13 +464,6 @@ setRunColorBuf (const System sys, int run, char *colorbuf)
   double h, l, s;
   int r, g, b;
 
-  // help function: contract roleoffset, roledelta with a factor (<= 1.0)
-  void contract (double factor)
-  {
-    roledelta = roledelta * factor;
-    roleoffset = (roleoffset * factor) + ((1.0 - factor) / 2.0);
-  }
-
   // determine #protocol, resulting in two colors
   {
     Termlist protocols;
@@ -547,12 +551,13 @@ setRunColorBuf (const System sys, int run, char *colorbuf)
       // Now this can result in a delta that is too high (depending on protocolrange)
       if (protrange * roledelta > RUNCOLORDELTA)
 	{
-	  contract (RUNCOLORDELTA / (protrange * roledelta));
+	  contract (roledelta, roleoffset,
+		    RUNCOLORDELTA / (protrange * roledelta));
 	}
     }
 
   // We slightly contract the colors (taking them away from protocol edges)
-  contract (RUNCOLORCONTRACT);
+  contract (roledelta, roleoffset, RUNCOLORCONTRACT);
 
   // Now we can convert this to a color
   color = protoffset + (protrange * roleoffset);
@@ -1061,27 +1066,29 @@ regularModifiedLabel (Binding b)
     }
 }
 
+void
+myarrow (const System sys, const int m0_from, const Binding b)
+{
+  if (m0_from)
+    {
+      eprintf ("\t");
+      intruderNodeM0 ();
+      eprintf (" -> ");
+      node (sys, b->run_to, b->ev_to);
+    }
+  else
+    {
+      arrow (sys, b);
+    }
+
+}
+
 //! Draw a single binding
 void
 drawBinding (const System sys, Binding b)
 {
   int intr_to, intr_from, m0_from;
 
-  void myarrow (const Binding b)
-  {
-    if (m0_from)
-      {
-	eprintf ("\t");
-	intruderNodeM0 ();
-	eprintf (" -> ");
-	node (sys, b->run_to, b->ev_to);
-      }
-    else
-      {
-	arrow (sys, b);
-      }
-
-  }
 
   intr_from = (sys->runs[b->run_from].protocol == INTRUDER);
   intr_to = (sys->runs[b->run_to].protocol == INTRUDER);
@@ -1121,7 +1128,7 @@ drawBinding (const System sys, Binding b)
 	{
 	  // intr->intr
 	  eprintf ("\t");
-	  myarrow (b);
+	  myarrow (sys, m0_from, b);
 	  eprintf (" [label=\"");
 	  termPrintRemap (b->term);
 	  eprintf ("\"");
@@ -1136,7 +1143,7 @@ drawBinding (const System sys, Binding b)
 	{
 	  // intr->regular
 	  eprintf ("\t");
-	  myarrow (b);
+	  myarrow (sys, m0_from, b);
 	  if (m0_from)
 	    {
 	      eprintf ("[weight=\"0.5\"]");
@@ -1151,7 +1158,7 @@ drawBinding (const System sys, Binding b)
 	{
 	  // regular->intr
 	  eprintf ("\t");
-	  myarrow (b);
+	  myarrow (sys, m0_from, b);
 	  eprintf (";\n");
 	}
       else
@@ -1163,7 +1170,7 @@ drawBinding (const System sys, Binding b)
 	  if (isCommunicationExact (sys, b))
 	    {
 	      eprintf ("\t");
-	      myarrow (b);
+	      myarrow (sys, m0_from, b);
 	      eprintf (" [style=bold,color=\"%s\"]", GOODCOMMCOLOR);
 	      eprintf (";\n");
 	    }
diff --git a/src/intruderknowledge.c b/src/intruderknowledge.c
index 9b362db..1b7278d 100644
--- a/src/intruderknowledge.c
+++ b/src/intruderknowledge.c
@@ -56,36 +56,25 @@ addEnumTerm (const System sys, Term t, Term actor, Termlist todo,
     {
       if (termSubTerm (t, todo->term))
 	{
-	  // Occurs, we have to iterate
-	  void iterateThis (Term to)
-	  {
-	    tolist = termlistPrepend (tolist, to);
-
-	    addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
-
-	    tolist = termlistDelTerm (tolist);
-	  }
+	  Termlist tl;
 
 	  fromlist = termlistPrepend (fromlist, todo->term);
 	  if (isTermEqual (todo->term, actor))
 	    {
 	      // Untrusted agents only
-	      Termlist tl;
-
-	      for (tl = sys->untrusted; tl != NULL; tl = tl->next)
-		{
-		  iterateThis (tl->term);
-		}
+	      tl = sys->untrusted;
 	    }
 	  else
 	    {
 	      // any agents
-	      Termlist tl;
-
-	      for (tl = sys->agentnames; tl != NULL; tl = tl->next)
-		{
-		  iterateThis (tl->term);
-		}
+	      tl = sys->agentnames;
+	    }
+	  while (tl != NULL)
+	    {
+	      tolist = termlistPrepend (tolist, tl->term);
+	      addEnumTerm (sys, t, actor, todo->next, fromlist, tolist);
+	      tolist = termlistDelTerm (tolist);
+	      tl = tl->next;
 	    }
 	  fromlist = termlistDelTerm (fromlist);
 	}
diff --git a/src/knowledge.c b/src/knowledge.c
index 255790b..300d61f 100644
--- a/src/knowledge.c
+++ b/src/knowledge.c
@@ -430,6 +430,14 @@ isKnowledgePublicFunction (const Knowledge know, const Term f)
   return inTermlist (know->publicfunctions, f);
 }
 
+Term
+funKey (Term orig, Term f)
+{
+  /* in: f'{op}, f
+   * out: f{op'} */
+  return makeTermFcall (termDuplicate (TermOp (orig)), termDuplicate (f));
+}
+
 //! Give the inverse key term of a term.
 /**
  * Gives a duplicate of the inverse Key of some term (which is used to encrypt something), as is defined
@@ -452,14 +460,6 @@ inverseKey (Knowledge know, Term key)
     {
       Termlist tl;
 
-      Term funKey (Term orig, Term f)
-      {
-	/* in: f'{op}, f
-	 * out: f{op'} */
-	return makeTermFcall (termDuplicate (TermOp (orig)),
-			      termDuplicate (f));
-      }
-
       tl = know->inversekeyfunctions;
       while (tl != NULL && tl->next != NULL)
 	{
diff --git a/src/mgu.c b/src/mgu.c
index 6dacb40..463b027 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -146,6 +146,22 @@ unify_callback_wrapper (Termlist tl, struct state_mgu_tmp *ptr_tmpstate)
 		ptr_tmpstate->oldcallback, ptr_tmpstate->oldstate);
 }
 
+int
+callsubst (int (*callback) (), void *state, Termlist tl, Term t, Term tsubst)
+{
+  int proceed;
+
+  t->subst = tsubst;
+#ifdef DEBUG
+  showSubst (t);
+#endif
+  tl = termlistAdd (tl, t);
+  proceed = callback (tl, state);
+  tl = termlistDelTerm (tl);
+  t->subst = NULL;
+  return proceed;
+}
+
 //! Most general unifier iteration
 /**
  * Try to determine the most general unifier of two terms, if so calls function.
@@ -161,21 +177,6 @@ unify_callback_wrapper (Termlist tl, struct state_mgu_tmp *ptr_tmpstate)
 int
 unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
 {
-  int callsubst (Termlist tl, Term t, Term tsubst)
-  {
-    int proceed;
-
-    t->subst = tsubst;
-#ifdef DEBUG
-    showSubst (t);
-#endif
-    tl = termlistAdd (tl, t);
-    proceed = callback (tl, state);
-    tl = termlistDelTerm (tl);
-    t->subst = NULL;
-    return proceed;
-  }
-
   /* added for speed */
   t1 = deVar (t1);
   t2 = deVar (t2);
@@ -223,7 +224,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
 	  t1 = t2;
 	  t2 = t3;
 	}
-      return callsubst (tl, t1, t2);
+      return callsubst (callback, state, tl, t1, t2);
     }
 
   /* symmetrical tests for single variable.
@@ -235,7 +236,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
 	return true;
       else
 	{
-	  return callsubst (tl, t2, t1);
+	  return callsubst (callback, state, tl, t2, t1);
 	}
     }
   if (realTermVariable (t1))
@@ -244,7 +245,7 @@ unify (Term t1, Term t2, Termlist tl, int (*callback) (), void *state)
 	return true;
       else
 	{
-	  return callsubst (tl, t1, t2);
+	  return callsubst (callback, state, tl, t1, t2);
 	}
     }
 
diff --git a/src/term.c b/src/term.c
index f39da5f..6bdd1b6 100644
--- a/src/term.c
+++ b/src/term.c
@@ -1188,6 +1188,53 @@ term_rolelocals_are_variables ()
   rolelocal_variable = 1;
 }
 
+//! Helper for counting encryption level of a term
+int
+iter_maxencrypt (Term baseterm, Term t)
+{
+  if (isTicketTerm (t))
+    {
+      return 0;
+    }
+  t = deVar (t);
+  if (t == NULL)
+    {
+#ifdef DEBUG
+      if (DEBUGL (2))
+	{
+	  eprintf ("Warning: Term encryption level finds a NULL for term ");
+	  termPrint (baseterm);
+	  eprintf ("\n");
+	}
+#endif
+      return 0;
+    }
+  if (realTermLeaf (t))
+    {
+      return 0;
+    }
+  else
+    {
+      int l, r;
+
+      if (realTermTuple (t))
+	{
+	  l = iter_maxencrypt (baseterm, TermOp1 (t));
+	  r = iter_maxencrypt (baseterm, TermOp2 (t));
+	}
+      else
+	{
+	  // encrypt
+	  l = 1 + iter_maxencrypt (baseterm, TermOp (t));
+	  r = iter_maxencrypt (baseterm, TermKey (t));
+	}
+      if (l > r)
+	return l;
+      else
+	return r;
+    }
+}
+
 //! Count the encryption level of a term
 /**
  * Note that this stops at any variable that is of ticket type.
@@ -1195,52 +1242,38 @@ term_rolelocals_are_variables ()
 int
 term_encryption_level (const Term term)
 {
-  int iter_maxencrypt (Term t)
-  {
-    if (isTicketTerm (t))
-      {
-	return 0;
-      }
-    t = deVar (t);
-    if (t == NULL)
-      {
-#ifdef DEBUG
-	if (DEBUGL (2))
-	  {
-	    eprintf ("Warning: Term encryption level finds a NULL for term ");
-	    termPrint (term);
-	    eprintf ("\n");
-	  }
-#endif
-	return 0;
-      }
-    if (realTermLeaf (t))
-      {
-	return 0;
-      }
-    else
-      {
-	int l, r;
+  return iter_maxencrypt (term, term);
+}
 
-	if (realTermTuple (t))
-	  {
-	    l = iter_maxencrypt (TermOp1 (t));
-	    r = iter_maxencrypt (TermOp2 (t));
-	  }
-	else
-	  {
-	    // encrypt
-	    l = 1 + iter_maxencrypt (TermOp (t));
-	    r = iter_maxencrypt (TermKey (t));
-	  }
-	if (l > r)
-	  return l;
-	else
-	  return r;
-      }
-  }
+struct ti_data
+{
+  int vars;
+  int structure;
+};
 
-  return iter_maxencrypt (term);
+void
+tcl_iterate (struct ti_data *p_data, Term t)
+{
+  t = deVar (t);
+  (p_data->structure)++;
+  if (realTermLeaf (t))
+    {
+      if (realTermVariable (t))
+	(p_data->vars)++;
+    }
+  else
+    {
+      if (realTermTuple (t))
+	{
+	  tcl_iterate (p_data, TermOp1 (t));
+	  tcl_iterate (p_data, TermOp2 (t));
+	}
+      else
+	{
+	  tcl_iterate (p_data, TermOp (t));
+	  tcl_iterate (p_data, TermKey (t));
+	}
+    }
 }
 
 //! Determine 'constrained factor' of a term
@@ -1252,40 +1285,61 @@ term_encryption_level (const Term term)
 float
 term_constrain_level (const Term term)
 {
-  int vars;
-  int structure;
-
-  void tcl_iterate (Term t)
-  {
-    t = deVar (t);
-    structure++;
-    if (realTermLeaf (t))
-      {
-	if (realTermVariable (t))
-	  vars++;
-      }
-    else
-      {
-	if (realTermTuple (t))
-	  {
-	    tcl_iterate (TermOp1 (t));
-	    tcl_iterate (TermOp2 (t));
-	  }
-	else
-	  {
-	    tcl_iterate (TermOp (t));
-	    tcl_iterate (TermKey (t));
-	  }
-      }
-  }
+  struct ti_data data;
 
   if (term == NULL)
     error ("Cannot determine constrain level of empty term.");
 
-  vars = 0;
-  structure = 0;
-  tcl_iterate (term);
-  return ((float) vars / (float) structure);
+  data.vars = 0;
+  data.structure = 0;
+  tcl_iterate (&data, term);
+  return ((float) data.vars / (float) data.structure);
+}
+
+void
+scan_levels (int level, Term t)
+{
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      int c;
+
+      c = 0;
+      while (c < level)
+	{
+	  eprintf ("  ");
+	  c++;
+	}
+      eprintf ("Scanning keylevel %i for term ", level);
+      termPrint (t);
+      eprintf ("\n");
+    }
+#endif
+  if (realTermLeaf (t))
+    {
+      Symbol sym;
+
+      // So, it occurs at 'level' as key. If that is less than known, store.
+      sym = TermSymb (t);
+      if (level < sym->keylevel)
+	{
+	  // New minimum level
+	  sym->keylevel = level;
+	}
+    }
+  else
+    {
+      if (realTermTuple (t))
+	{
+	  scan_levels (level, TermOp1 (t));
+	  scan_levels (level, TermOp2 (t));
+	}
+      else
+	{
+	  scan_levels (level, TermOp (t));
+	  scan_levels ((level + 1), TermKey (t));
+	}
+    }
 }
 
 //! Adjust the keylevels of the symbols in a term.
@@ -1295,54 +1349,22 @@ term_constrain_level (const Term term)
 void
 term_set_keylevels (const Term term)
 {
-  void scan_levels (int level, Term t)
-  {
-#ifdef DEBUG
-    if (DEBUGL (5))
-      {
-	int c;
-
-	c = 0;
-	while (c < level)
-	  {
-	    eprintf ("  ");
-	    c++;
-	  }
-	eprintf ("Scanning keylevel %i for term ", level);
-	termPrint (t);
-	eprintf ("\n");
-      }
-#endif
-    if (realTermLeaf (t))
-      {
-	Symbol sym;
-
-	// So, it occurs at 'level' as key. If that is less than known, store.
-	sym = TermSymb (t);
-	if (level < sym->keylevel)
-	  {
-	    // New minimum level
-	    sym->keylevel = level;
-	  }
-      }
-    else
-      {
-	if (realTermTuple (t))
-	  {
-	    scan_levels (level, TermOp1 (t));
-	    scan_levels (level, TermOp2 (t));
-	  }
-	else
-	  {
-	    scan_levels (level, TermOp (t));
-	    scan_levels ((level + 1), TermKey (t));
-	  }
-      }
-  }
-
   scan_levels (0, term);
 }
 
+void
+termFromTo (Term t1, Term t2)
+{
+  t1 = deVar (t1);
+  t2 = deVar (t2);
+
+  eprintf (" [");
+  termPrint (t1);
+  eprintf ("]->[");
+  termPrint (t2);
+  eprintf ("] ");
+}
+
 //! Print the term diff of two terms
 /**
  * This is not correct yet. We need to add function application and correct tuple handing.
@@ -1350,18 +1372,6 @@ term_set_keylevels (const Term term)
 void
 termPrintDiff (Term t1, Term t2)
 {
-  void termFromTo (Term t1, Term t2)
-  {
-    t1 = deVar (t1);
-    t2 = deVar (t2);
-
-    eprintf (" [");
-    termPrint (t1);
-    eprintf ("]->[");
-    termPrint (t2);
-    eprintf ("] ");
-  }
-
   t1 = deVar (t1);
   t2 = deVar (t2);
 
diff --git a/src/xmlout.c b/src/xmlout.c
index a41a5fb..6b01062 100644
--- a/src/xmlout.c
+++ b/src/xmlout.c
@@ -843,6 +843,71 @@ xmlRunInfo (const System sys, const int run)
   xmlRunVariables (sys, run);
 }
 
+//! Test whether to display this event
+/**
+ * Could be integrated into a single line on the while loop,
+ * but that makes it rather hard to understand.
+ */
+int
+showthis (const System sys, const int run, const Roledef rd, const int index)
+{
+  if (rd != NULL)
+    {
+      if (index < sys->runs[run].step)
+	{
+	  return true;
+	}
+      else
+	{
+	  if (switches.extendTrivial || switches.extendNonRecvs)
+	    {
+	      if (rd->type != RECV)
+		{
+		  return true;
+		}
+	      else
+		{
+		  if (switches.extendTrivial)
+		    {
+		      /* This is a recv, and we don't know whether to
+		       * include it. Default behaviour would be to jump
+		       * out of the conditions, and return false.
+		       * Instead, we check whether it can be trivially
+		       * satisfied by the knowledge from the preceding
+		       * events.
+		       */
+		      if (isTriviallyKnownAtArachne (sys,
+						     rd->message, run, index))
+			{
+			  return true;
+			}
+		      else
+			{
+			  /* We cannot extend it trivially, based on
+			   * the preceding events, but maybe we can
+			   * base it on another (*all*) event. That
+			   * would in fact introduce another implicit
+			   * binding. Currently, we do not explicitly
+			   * introduce this binding, but just allow
+			   * displaying the event.
+			   *
+			   * TODO consider what it means to leave out
+			   * this binding.
+			   */
+			  if (isTriviallyKnownAfterArachne
+			      (sys, rd->message, run, index))
+			    {
+			      return true;
+			    }
+			}
+		    }
+		}
+	    }
+	}
+    }
+  return false;
+}
+
 //! Display runs
 void
 xmlOutRuns (const System sys)
@@ -862,74 +927,9 @@ xmlOutRuns (const System sys)
 	Roledef rd;
 	int index;
 
-	//! Test whether to display this event
-	/**
-	 * Could be integrated into a single line on the while loop,
-	 * but that makes it rather hard to understand.
-	 */
-	int showthis (void)
-	{
-	  if (rd != NULL)
-	    {
-	      if (index < sys->runs[run].step)
-		{
-		  return true;
-		}
-	      else
-		{
-		  if (switches.extendTrivial || switches.extendNonRecvs)
-		    {
-		      if (rd->type != RECV)
-			{
-			  return true;
-			}
-		      else
-			{
-			  if (switches.extendTrivial)
-			    {
-			      /* This is a recv, and we don't know whether to
-			       * include it. Default behaviour would be to jump
-			       * out of the conditions, and return false.
-			       * Instead, we check whether it can be trivially
-			       * satisfied by the knowledge from the preceding
-			       * events.
-			       */
-			      if (isTriviallyKnownAtArachne (sys,
-							     rd->message,
-							     run, index))
-				{
-				  return true;
-				}
-			      else
-				{
-				  /* We cannot extend it trivially, based on
-				   * the preceding events, but maybe we can
-				   * base it on another (*all*) event. That
-				   * would in fact introduce another implicit
-				   * binding. Currently, we do not explicitly
-				   * introduce this binding, but just allow
-				   * displaying the event.
-				   *
-				   * TODO consider what it means to leave out
-				   * this binding.
-				   */
-				  if (isTriviallyKnownAfterArachne
-				      (sys, rd->message, run, index))
-				    {
-				      return true;
-				    }
-				}
-			    }
-			}
-		    }
-		}
-	    }
-	  return false;
-	}
-
 	index = 0;
 	rd = sys->runs[run].start;
-	while (showthis ())
+	while (showthis (sys, run, rd, index))
 	  {
 	    xmlOutEvent (sys, rd, run, index);
 	    index++;