diff --git a/src/arachne.c b/src/arachne.c
index 657684a..20a52af 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -188,7 +188,8 @@ int
 isTermFunctionName (Term t)
 {
   t = deVar (t);
-  if (t != NULL && isTermLeaf(t) && t->stype != NULL && inTermlist (t->stype, TERM_Function))
+  if (t != NULL && isTermLeaf (t) && t->stype != NULL
+      && inTermlist (t->stype, TERM_Function))
     return 1;
   return 0;
 }
@@ -200,9 +201,9 @@ getTermFunction (Term t)
   t = deVar (t);
   if (t != NULL)
     {
-      if (realTermEncrypt (t) && isTermFunctionName (TermKey(t)))
+      if (realTermEncrypt (t) && isTermFunctionName (TermKey (t)))
 	{
-	  return TermKey(t);
+	  return TermKey (t);
 	}
     }
   return NULL;
@@ -304,7 +305,7 @@ determine_unification_run (Termlist tl)
   while (tl != NULL)
     {
       //! Again, hardcoded reference to compiler.c. Level -3 means a local constant for a role.
-      if (tl->term->type != VARIABLE && TermRunid(tl->term) == -3)
+      if (tl->term->type != VARIABLE && TermRunid (tl->term) == -3)
 	{
 	  Term t;
 
@@ -320,12 +321,12 @@ determine_unification_run (Termlist tl)
 	      if (run == -2)
 		{
 		  // Any run
-		  run = TermRunid(t);
+		  run = TermRunid (t);
 		}
 	      else
 		{
 		  // Specific run: compare
-		  if (run != TermRunid(t))
+		  if (run != TermRunid (t))
 		    {
 		      return -1;
 		    }
@@ -553,7 +554,7 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 	    if (realTermEncrypt (tl->term))
 	      {
 		/* the key is a construction itself */
-		if (inKnowledge (sys->know, TermKey(tl->term)))
+		if (inKnowledge (sys->know, TermKey (tl->term)))
 		  {
 		    /* the key is constructed by a public thing */
 		    /* typically, this is a public key, so we postpone it  */
@@ -561,7 +562,9 @@ bind_existing_to_goal (const Binding b, const int run, const int index)
 		  }
 	      }
 	    /* add the key as a goal */
-	    newgoals = newgoals + goal_add (tl->term, b->run_to, b->ev_to, prioritylevel);
+	    newgoals =
+	      newgoals + goal_add (tl->term, b->run_to, b->ev_to,
+				   prioritylevel);
 	    tl = tl->next;
 	  }
 
@@ -720,10 +723,11 @@ dotSemiState ()
   goal_graph_create ();		// create graph
   if (warshall (graph, nodes) == 0)	// determine closure
     {
-      eprintf ("// This graph was not completely closed transitively because it contains a cycle!\n");
+      eprintf
+	("// This graph was not completely closed transitively because it contains a cycle!\n");
     }
 
-  ranks = memAlloc (nodes * sizeof(int));
+  ranks = memAlloc (nodes * sizeof (int));
   maxrank = graph_ranks (graph, ranks, nodes);	// determine ranks
 
 #ifdef DEBUG
@@ -731,57 +735,56 @@ dotSemiState ()
   printSemiState ();
   // Even draw all dependencies for non-intruder runs
   // Real nice debugging :(
-    {
-      int run;
+  {
+    int run;
 
-      run = 0;
-      while (run < sys->maxruns)
-	{
-	  int ev;
+    run = 0;
+    while (run < sys->maxruns)
+      {
+	int ev;
 
-	  ev = 0;
-	  while (ev < sys->runs[run].length)
-	    {
-	      int run2;
-	      int notfirstrun;
+	ev = 0;
+	while (ev < sys->runs[run].length)
+	  {
+	    int run2;
+	    int notfirstrun;
 
-	      eprintf ("// precedence: r%ii%i <- ", run,ev);
-	      run2 = 0;
-	      notfirstrun = 0;
-	      while (run2 < sys->maxruns)
-		{
-		  int notfirstev;
-		  int ev2;
+	    eprintf ("// precedence: r%ii%i <- ", run, ev);
+	    run2 = 0;
+	    notfirstrun = 0;
+	    while (run2 < sys->maxruns)
+	      {
+		int notfirstev;
+		int ev2;
 
-		  notfirstev = 0;
-		  ev2 = 0;
-		  while (ev2 < sys->runs[run2].length)
-		    {
-		      if (graph[graph_nodes (nodes, run2, ev2, run, ev)]
-			  != 0)
-			{
-			  if (notfirstev)
-			      eprintf (",");
-			  else
-			    {
-			      if (notfirstrun)
-				  eprintf (" ");
-			      eprintf ("r%i:", run2);
-			    }
-			  eprintf ("%i", ev2);
-			  notfirstrun = 1;
-			  notfirstev = 1;
-			}
-		      ev2++;
-		    }
-		  run2++;
-		}
-	      eprintf ("\n");
-	      ev++;
-	    }
-	  run++;
-	}
-    }
+		notfirstev = 0;
+		ev2 = 0;
+		while (ev2 < sys->runs[run2].length)
+		  {
+		    if (graph[graph_nodes (nodes, run2, ev2, run, ev)] != 0)
+		      {
+			if (notfirstev)
+			  eprintf (",");
+			else
+			  {
+			    if (notfirstrun)
+			      eprintf (" ");
+			    eprintf ("r%i:", run2);
+			  }
+			eprintf ("%i", ev2);
+			notfirstrun = 1;
+			notfirstev = 1;
+		      }
+		    ev2++;
+		  }
+		run2++;
+	      }
+	    eprintf ("\n");
+	    ev++;
+	  }
+	run++;
+      }
+  }
 #endif
 
   // Draw graph
@@ -799,22 +802,22 @@ dotSemiState ()
 	  // Regular run
 
 	  /* DISABLED subgraphs
-	  eprintf ("\tsubgraph cluster_run%i {\n", run);
-	  eprintf ("\t\tlabel = \"");
-	  eprintf ("#%i: ", run);
-	  termPrint (sys->runs[run].protocol->nameterm);
-	  eprintf (", ");
-	  agentsOfRunPrint (sys, run);
-	  eprintf ("\";\n", run);
-	  if (run == 0)
-	    {
-	      eprintf ("\t\tcolor = red;\n");
-	    }
-	  else
-	    {
-	      eprintf ("\t\tcolor = blue;\n");
-	    }
-	    */
+	     eprintf ("\tsubgraph cluster_run%i {\n", run);
+	     eprintf ("\t\tlabel = \"");
+	     eprintf ("#%i: ", run);
+	     termPrint (sys->runs[run].protocol->nameterm);
+	     eprintf (", ");
+	     agentsOfRunPrint (sys, run);
+	     eprintf ("\";\n", run);
+	     if (run == 0)
+	     {
+	     eprintf ("\t\tcolor = red;\n");
+	     }
+	     else
+	     {
+	     eprintf ("\t\tcolor = blue;\n");
+	     }
+	   */
 
 
 	  // Display the respective events
@@ -883,7 +886,7 @@ dotSemiState ()
 			}
 		      // Draw the first box
 		      // This used to be drawn only if done && send_before_read, now we always draw it.
-		      eprintf ("\t\ts%i [label=\"Run %i\\n", run,run);
+		      eprintf ("\t\ts%i [label=\"Run %i\\n", run, run);
 		      agentsOfRunPrint (sys, run);
 		      eprintf ("\", shape=diamond];\n");
 		      eprintf ("\t\ts%i -> ", run);
@@ -895,8 +898,8 @@ dotSemiState ()
 	      rd = rd->next;
 	    }
 	  /* DISABLED subgraphs
-	  eprintf ("\t}\n");
-	  */
+	     eprintf ("\t}\n");
+	   */
 	}
       run++;
     }
@@ -983,7 +986,7 @@ dotSemiState ()
 			    }
 			  if (other_route == 0)
 			    {
-			      Roledef rd,rd2;
+			      Roledef rd, rd2;
 			      /*
 			       * We have decided to draw this binding,
 			       * from run2,ev2 to run,ev
@@ -995,8 +998,9 @@ dotSemiState ()
 			      node (run, ev);
 			      eprintf (" ");
 			      // decide color
-		              rd = roledef_shift (sys->runs[run].start,ev);
-		              rd2 = roledef_shift (sys->runs[run2].start,ev2);
+			      rd = roledef_shift (sys->runs[run].start, ev);
+			      rd2 =
+				roledef_shift (sys->runs[run2].start, ev2);
 			      if (rd->type == CLAIM)
 				{
 				  // Towards a claim, so only indirect dependency
@@ -1009,9 +1013,13 @@ dotSemiState ()
 				  if (rd->type == READ && rd2->type == SEND)
 				    {
 				      // We want to distinguish where it is from a 'broken' send
-				      if (isTermEqual (rd->message, rd2->message))
+				      if (isTermEqual
+					  (rd->message, rd2->message))
 					{
-					  if (isTermEqual (rd->from, rd2->from) && isTermEqual (rd->to, rd2->to))
+					  if (isTermEqual
+					      (rd->from, rd2->from)
+					      && isTermEqual (rd->to,
+							      rd2->to))
 					    {
 					      // Wow, a perfect match. Leave the arrow as-is :)
 					      eprintf ("[color=forestgreen]");
@@ -1019,13 +1027,15 @@ dotSemiState ()
 					  else
 					    {
 					      // Same message, different people
-					      eprintf ("[label=\"redirect\",color=darkorange2]");
+					      eprintf
+						("[label=\"redirect\",color=darkorange2]");
 					    }
 					}
 				      else
 					{
 					  // Not even the same message, intruder construction
-					  eprintf ("[label=\"construct\",color=red]");
+					  eprintf
+					    ("[label=\"construct\",color=red]");
 					}
 				    }
 				}
@@ -1039,9 +1049,10 @@ dotSemiState ()
 			      run3--;
 			      ev3--;
 
-			      eprintf ("\t// HIDDEN r%ii%i -> r%ii%i because route through r%ii%i\n",
-				       run2, ev2, run, ev, run3, ev3);
-			      
+			      eprintf
+				("\t// HIDDEN r%ii%i -> r%ii%i because route through r%ii%i\n",
+				 run2, ev2, run, ev, run3, ev3);
+
 			    }
 #endif
 			}
@@ -1055,62 +1066,62 @@ dotSemiState ()
     }
 
   // Third, all ranking info
-    {
-      int myrank;
+  {
+    int myrank;
 
 #ifdef DEBUG
+    {
+      int n;
+
+      eprintf ("/* ranks: %i\n", maxrank);
+      n = 0;
+      while (n < nodes)
 	{
-	  int n;
-
-	  eprintf ("/* ranks: %i\n", maxrank);
-	  n = 0;
-	  while (n < nodes)
-	    {
-	      eprintf ("%i ", ranks[n]);
-	      n++;
-	    }
-	  eprintf ("\n*/\n\n");
-	}
-#endif
-      myrank = 0;
-      while (myrank < maxrank)
-	{
-	  int count;
-	  int run;
-	  int run1;
-	  int ev1;
-
-	  count = 0;
-	  run = 0;
-	  while (run < sys->maxruns)
-	    {
-	      if (sys->runs[run].protocol != INTRUDER)
-		{
-		  int ev;
-
-		  ev = 0;
-		  while (ev < sys->runs[run].step)
-		    {
-		      if (myrank == ranks[node_number (run,ev)])
-			{
-			  if (count == 0)
-			      eprintf ("\t{ rank = same; ");
-			  count++;
-			  eprintf ("r%ii%i; ",run,ev);
-			}
-		      ev++;
-		    }
-		}
-	      run++;
-	    }
-	  if (count > 0)
-	      eprintf ("}\t\t// rank %i\n", myrank);
-	  myrank++;
+	  eprintf ("%i ", ranks[n]);
+	  n++;
 	}
+      eprintf ("\n*/\n\n");
     }
-  
+#endif
+    myrank = 0;
+    while (myrank < maxrank)
+      {
+	int count;
+	int run;
+	int run1;
+	int ev1;
+
+	count = 0;
+	run = 0;
+	while (run < sys->maxruns)
+	  {
+	    if (sys->runs[run].protocol != INTRUDER)
+	      {
+		int ev;
+
+		ev = 0;
+		while (ev < sys->runs[run].step)
+		  {
+		    if (myrank == ranks[node_number (run, ev)])
+		      {
+			if (count == 0)
+			  eprintf ("\t{ rank = same; ");
+			count++;
+			eprintf ("r%ii%i; ", run, ev);
+		      }
+		    ev++;
+		  }
+	      }
+	    run++;
+	  }
+	if (count > 0)
+	  eprintf ("}\t\t// rank %i\n", myrank);
+	myrank++;
+      }
+  }
+
   // clean memory
-  memFree (ranks, nodes * sizeof(int));		// ranks
+  memFree (ranks, nodes * sizeof (int));	// ranks
 
   // close graph
   eprintf ("};\n\n");
@@ -1225,8 +1236,8 @@ select_goal ()
       b = (Binding) bl->data;
 
       // Ignore singular variables
-      if (!b->done && !realTermVariable (deVar(b->term)) )
-      //if (!b->done)
+      if (!b->done && !realTermVariable (deVar (b->term)))
+	//if (!b->done)
 	{
 	  float cons;
 
@@ -1361,8 +1372,8 @@ bind_goal_new_encrypt (const Binding b)
 	}
 
       // must be encryption
-      t1 = TermOp(term);
-      t2 = TermKey(term);
+      t1 = TermOp (term);
+      t2 = TermKey (term);
 
       if (t2 != TERM_Hidden)
 	{
@@ -1481,7 +1492,8 @@ bind_goal_regular_run (const Binding b)
       }
 #endif
     if (!termMguSubTerm
-	(b->term, rd->message, test_sub_unification, sys->know->inverses, NULL))
+	(b->term, rd->message, test_sub_unification, sys->know->inverses,
+	 NULL))
       {
 	int sflag;
 
@@ -1665,12 +1677,14 @@ prune_theorems ()
 	{
 	  Term agent;
 
-	  agent = deVar(agl->term);
+	  agent = deVar (agl->term);
 	  if (agent == NULL)
 	    {
 	      error ("Agent of run %i is NULL", run);
 	    }
-	  if (!realTermLeaf (agent) || (agent->stype != NULL && !inTermlist (agent->stype, TERM_Agent)))
+	  if (!realTermLeaf (agent)
+	      || (agent->stype != NULL
+		  && !inTermlist (agent->stype, TERM_Agent)))
 	    {
 	      if (sys->output == PROOF)
 		{
@@ -1718,9 +1732,9 @@ prune_theorems ()
 	    {
 	      if (sys->runs[run].agents != NULL)
 		{
-	          Term actor;
+		  Term actor;
 
-		  actor = agentOfRun(sys, run);
+		  actor = agentOfRun (sys, run);
 		  if (actor == NULL)
 		    {
 		      error ("Agent of run %i is NULL", run);
@@ -1730,7 +1744,9 @@ prune_theorems ()
 		      if (sys->output == PROOF)
 			{
 			  indentPrint ();
-			  eprintf ("Pruned because the actor of run %i is untrusted.\n", run);
+			  eprintf
+			    ("Pruned because the actor of run %i is untrusted.\n",
+			     run);
 			}
 		      return 1;
 		    }
@@ -1741,7 +1757,7 @@ prune_theorems ()
 
 		  globalError++;
 		  eprintf ("Run %i: ", run);
-                  role_name_print (run);
+		  role_name_print (run);
 		  eprintf (" has an empty agents list.\n");
 		  eprintf ("protocol->rolenames: ");
 		  p = (Protocol) sys->runs[run].protocol;
@@ -1847,7 +1863,8 @@ prune_bounds ()
       if (sys->output == PROOF)
 	{
 	  indentPrint ();
-	  eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n", proofDepth, sys->switch_maxtracelength);
+	  eprintf ("Pruned: proof tree too deep: %i (-l %i switch)\n",
+		   proofDepth, sys->switch_maxtracelength);
 	}
       return 1;
     }
diff --git a/src/binding.c b/src/binding.c
index 9792291..047bb63 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -177,7 +177,7 @@ goal_graph_create ()
 		      Term t;
 
 		      t = tl->term;
-		      if (t->type == VARIABLE && TermRunid(t) == run
+		      if (t->type == VARIABLE && TermRunid (t) == run
 			  && t->subst != NULL)
 			{
 			  // t is a variable of run
@@ -190,7 +190,7 @@ goal_graph_create ()
 
 			      t2 = tl2->term;
 			      if (realTermLeaf (t2) && t2->type != VARIABLE
-				  && TermRunid(t2) == run2)
+				  && TermRunid (t2) == run2)
 				{
 				  // t2 is a constant of run2
 				  if (isTermEqual (t, t2))
@@ -250,20 +250,28 @@ goal_graph_create ()
 						      else
 							{
 							  // It doesn't occur first in a READ, which shouldn't be happening
-							  if (sys->output == PROOF)
+							  if (sys->output ==
+							      PROOF)
 							    {
-							      eprintf ("Term ");
+							      eprintf
+								("Term ");
 							      termPrint (t2);
-							      eprintf (" from run %i occurs in run %i, term ",
+							      eprintf
+								(" from run %i occurs in run %i, term ",
 								 run2, run);
 							      termPrint (t);
-							      eprintf (" before it is read?\n");
+							      eprintf
+								(" before it is read?\n");
 							    }
 							  // Thus, we create an artificial loop
-							  if (sys->runs[0].step > 1)
+							  if (sys->runs[0].
+							      step > 1)
 							    {
 							      // This forces a loop, and thus prunes
-							      graph[graph_nodes (nodes, 0,1, 0,0)] = 1;
+							      graph
+								[graph_nodes
+								 (nodes, 0, 1,
+								  0, 0)] = 1;
 							    }
 							}
 						    }
@@ -421,21 +429,19 @@ goal_add (Term term, const int run, const int ev, const int level)
       int nope;
 
       int testSame (void *data)
-	{
-	  Binding b;
+      {
+	Binding b;
 
-	  b = (Binding) data;
-	  if (isTermEqual (b->term, term) &&
-	      run == b->run_to &&
-	      ev == b->ev_to)
-	    { // abort scan, report
-	      return 0;
-	    }
-	  else
-	    { // proceed with scan
-	      return 1;
-	    }
-	}
+	b = (Binding) data;
+	if (isTermEqual (b->term, term) && run == b->run_to && ev == b->ev_to)
+	  {			// abort scan, report
+	    return 0;
+	  }
+	else
+	  {			// proceed with scan
+	    return 1;
+	  }
+      }
 
       nope = list_iterate (sys->bindings, testSame);
       if (nope)
diff --git a/src/claim.h b/src/claim.h
index c6c7acd..c1c0f94 100644
--- a/src/claim.h
+++ b/src/claim.h
@@ -3,7 +3,9 @@
 
 int check_claim_nisynch (const System sys, const int i);
 int check_claim_niagree (const System sys, const int i);
-int arachne_claim_niagree (const System sys, const int claim_run, const int claim_index);
-int arachne_claim_nisynch (const System sys, const int claim_run, const int claim_index);
+int arachne_claim_niagree (const System sys, const int claim_run,
+			   const int claim_index);
+int arachne_claim_nisynch (const System sys, const int claim_run,
+			   const int claim_index);
 
 #endif
diff --git a/src/compiler.c b/src/compiler.c
index b5af343..ca2154b 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -241,7 +241,7 @@ levelFind (Symbol s, int level)
     {
       if (isTermLeaf (tl->term))
 	{
-	  if (TermSymb(tl->term) == s)
+	  if (TermSymb (tl->term) == s)
 	    {
 	      return tl->term;
 	    }
@@ -404,8 +404,7 @@ commEvent (int event, Tac tc)
 	{
 	  /* we already had this label constant */
 	  /* leaves a garbage tuple. dunnoh what to do with it */
-	  label =
-	    makeTermTuple (thisProtocol->nameterm, label);
+	  label = makeTermTuple (thisProtocol->nameterm, label);
 	}
     }
   /**
@@ -441,9 +440,11 @@ commEvent (int event, Tac tc)
 	{
 	  /* set sendrole */
 	  if (!isTermEqual (fromrole, thisRole->nameterm))
-	      error ("Send role does not correspond to execution role at line %i.", tc->lineno);
+	    error
+	      ("Send role does not correspond to execution role at line %i.",
+	       tc->lineno);
 	  if (linfo->sendrole != NULL)
-	      error ("Label defined twice for sendrole!");
+	    error ("Label defined twice for sendrole!");
 	  linfo->sendrole = fromrole;
 
 	  /* set keylevels based on send events */
@@ -456,9 +457,11 @@ commEvent (int event, Tac tc)
 	  // READ
 	  /* set readrole */
 	  if (!isTermEqual (torole, thisRole->nameterm))
-	      error ("Read role does not correspond to execution role at line %i.", tc->lineno);
+	    error
+	      ("Read role does not correspond to execution role at line %i.",
+	       tc->lineno);
 	  if (linfo->readrole != NULL)
-	      error ("Label defined twice for readrole!");
+	    error ("Label defined twice for readrole!");
 	  linfo->readrole = torole;
 	}
 
@@ -505,7 +508,7 @@ commEvent (int event, Tac tc)
       else
 	{
 	  /* n parameters */
-	  msg = TermOp2(deVar (claimbig));
+	  msg = TermOp2 (deVar (claimbig));
 	  if (tupleCount (msg) != n)
 	    {
 	      error ("Problem with claim tuple unfolding at line %i.",
@@ -540,7 +543,8 @@ commEvent (int event, Tac tc)
       cl->rolename = fromrole;
       cl->role = thisRole;
       if (!isTermEqual (fromrole, thisRole->nameterm))
-	  error ("Claim role does not correspond to execution role at line %i.", tc->lineno);
+	error ("Claim role does not correspond to execution role at line %i.",
+	       tc->lineno);
       cl->roledef = NULL;
       cl->count = 0;
       cl->complete = 0;
@@ -690,7 +694,7 @@ runInstanceCreate (Tac tc)
   /* first, locate the protocol */
   psym = tc->t1.tac->t1.sym;
   p = sys->protocols;
-  while (p != NULL && TermSymb(p->nameterm) != psym)
+  while (p != NULL && TermSymb (p->nameterm) != psym)
     p = p->next;
   if (p == NULL)
     {
@@ -703,7 +707,7 @@ runInstanceCreate (Tac tc)
   /* locate the role */
   rsym = tc->t1.tac->t2.sym;
   r = p->roles;
-  while (r != NULL && TermSymb(r->nameterm) != rsym)
+  while (r != NULL && TermSymb (r->nameterm) != rsym)
     r = r->next;
   if (r == NULL)
     {
@@ -935,7 +939,7 @@ compute_role_variables (const System sys, Protocol p, Role r)
 }
 
 //! Compute term list of rolenames involved in a given term list of labels
-Termlist 
+Termlist
 compute_label_roles (Termlist labels)
 {
   Termlist roles;
@@ -948,7 +952,7 @@ compute_label_roles (Termlist labels)
       linfo = label_find (sys->labellist, labels->term);
 #ifdef DEBUG
       if (linfo == NULL)
-	  error ("Label in prec list not found in label info list");
+	error ("Label in prec list not found in label info list");
 #endif
       roles = termlistAddNew (roles, linfo->sendrole);
       roles = termlistAddNew (roles, linfo->readrole);
@@ -977,7 +981,8 @@ order_label_roles (const Claimlist cl)
 #endif
   roles_remaining = termlistShallow (cl->roles);
   roles_ordered = termlistAdd (NULL, cl->rolename);
-  roles_remaining = termlistDelTerm (termlistFind (roles_remaining, cl->rolename));
+  roles_remaining =
+    termlistDelTerm (termlistFind (roles_remaining, cl->rolename));
 
   distance = 0;
   while (roles_remaining != NULL)
@@ -991,40 +996,42 @@ order_label_roles (const Claimlist cl)
 #endif
 
       int scan_label (void *data)
-	{
-	  Labelinfo linfo;
+      {
+	Labelinfo linfo;
 
-	  linfo = (Labelinfo) data;
-	  if (inTermlist (cl->prec, linfo->label ))
-	    {
-	      if (linfo->protocol == cl->protocol)
+	linfo = (Labelinfo) data;
+	if (inTermlist (cl->prec, linfo->label))
+	  {
+	    if (linfo->protocol == cl->protocol)
+	      {
+		// 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 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))
 		    {
-		      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));
+		      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->readrole);
-		  roles_test (linfo->readrole, linfo->sendrole);
 		}
-	    }
-	  return 1;
-	}
+
+		roles_test (linfo->sendrole, linfo->readrole);
+		roles_test (linfo->readrole, linfo->sendrole);
+	      }
+	  }
+	return 1;
+      }
 
       list_iterate (sys->labellist, scan_label);
     }
@@ -1417,7 +1424,7 @@ compute_prec_sets (const System sys)
 	    {
 	      Protocol p;
 
-	      printf ("Preceding label set for r:%i, ev:%i = ", r1,ev1);
+	      printf ("Preceding label set for r:%i, ev:%i = ", r1, ev1);
 	      termlistPrint (cl->prec);
 	      printf (", involving roles ");
 	      termlistPrint (cl->roles);
diff --git a/src/knowledge.c b/src/knowledge.c
index 4b2efdc..ede0c1a 100644
--- a/src/knowledge.c
+++ b/src/knowledge.c
@@ -154,8 +154,8 @@ knowledgeAddTerm (Knowledge know, Term term)
     {
       int status;
 
-      status = knowledgeAddTerm (know, TermOp1(term));
-      return knowledgeAddTerm (know, TermOp2(term)) || status;
+      status = knowledgeAddTerm (know, TermOp1 (term));
+      return knowledgeAddTerm (know, TermOp2 (term)) || status;
     }
 
   /* test whether we knew it before */
@@ -172,12 +172,12 @@ knowledgeAddTerm (Knowledge know, Term term)
     }
   if (term->type == ENCRYPT)
     {
-      Term invkey = inverseKey (know->inverses, TermKey(term));
+      Term invkey = inverseKey (know->inverses, TermKey (term));
       if (inKnowledge (know, invkey))
 	{
 	  /* we can decrypt it */
-	  knowledgeAddTerm (know, TermOp(term));
-	  if (!inKnowledge (know, TermKey(term)))
+	  knowledgeAddTerm (know, TermOp (term));
+	  if (!inKnowledge (know, TermKey (term)))
 	    {
 	      /* we know the op now, but not the key, so add it anyway */
 	      know->encrypt = termlistAdd (know->encrypt, term);
@@ -208,9 +208,9 @@ knowledgeSimplify (Knowledge know, Term key)
 
   while (scan != NULL)
     {
-      if (isTermEqual (TermKey(scan->term), invkey))
+      if (isTermEqual (TermKey (scan->term), invkey))
 	{
-	  tldecrypts = termlistAdd (tldecrypts, TermOp(scan->term));
+	  tldecrypts = termlistAdd (tldecrypts, TermOp (scan->term));
 	  know->encrypt = termlistDelTerm (scan);
 	  scan = know->encrypt;
 	}
@@ -285,14 +285,14 @@ inKnowledge (const Knowledge know, Term term)
   if (term->type == ENCRYPT)
     {
       return inTermlist (know->encrypt, term) ||
-	(inKnowledge (know, TermKey(term))
-	 && inKnowledge (know, TermOp(term)));
+	(inKnowledge (know, TermKey (term))
+	 && inKnowledge (know, TermOp (term)));
     }
   if (term->type == TUPLE)
     {
       return (inTermlist (know->encrypt, term) ||
-	      (inKnowledge (know, TermOp1(term)) &&
-	       inKnowledge (know, TermOp2(term))));
+	      (inKnowledge (know, TermOp1 (term)) &&
+	       inKnowledge (know, TermOp2 (term))));
     }
   return 0;			/* unrecognized term type, weird */
 }
diff --git a/src/label.c b/src/label.c
index e0d5077..3358b3d 100644
--- a/src/label.c
+++ b/src/label.c
@@ -9,7 +9,8 @@
 #include "system.h"
 
 //! Create a new labelinfo node
-Labelinfo label_create (const Term label, const Protocol protocol)
+Labelinfo
+label_create (const Term label, const Protocol protocol)
 {
   Labelinfo li;
 
@@ -22,31 +23,33 @@ Labelinfo label_create (const Term label, const Protocol protocol)
 }
 
 //! Destroy a labelinfo node
-void label_destroy (Labelinfo linfo)
+void
+label_destroy (Labelinfo linfo)
 {
   memFree (linfo, sizeof (struct labelinfo));
 }
 
 //! Given a list of label infos, yield the correct one or NULL
-Labelinfo label_find (List labellist, const Term label)
+Labelinfo
+label_find (List labellist, const Term label)
 {
   Labelinfo linfo;
 
   int label_find_scan (void *data)
-    {
-      Labelinfo linfo_scan;
+  {
+    Labelinfo linfo_scan;
 
-      linfo_scan = (Labelinfo) data;
-      if (isTermEqual (label, linfo_scan->label))
-	{
-	  linfo = linfo_scan;
-	  return 0;
-	}
-      else
-	{
-	  return 1;
-	}
-    }
+    linfo_scan = (Labelinfo) data;
+    if (isTermEqual (label, linfo_scan->label))
+      {
+	linfo = linfo_scan;
+	return 0;
+      }
+    else
+      {
+	return 1;
+      }
+  }
 
   linfo = NULL;
   if (label != NULL)
@@ -55,4 +58,3 @@ Labelinfo label_find (List labellist, const Term label)
     }
   return linfo;
 }
-
diff --git a/src/label.h b/src/label.h
index b74f70d..434a1e3 100644
--- a/src/label.h
+++ b/src/label.h
@@ -10,13 +10,13 @@
  */
 struct labelinfo
 {
-    Term label;
-    Protocol protocol;
-    Term sendrole;
-    Term readrole;
+  Term label;
+  Protocol protocol;
+  Term sendrole;
+  Term readrole;
 };
 
-typedef struct labelinfo* Labelinfo;
+typedef struct labelinfo *Labelinfo;
 
 Labelinfo label_create (const Term label, const Protocol protocol);
 void label_destroy (Labelinfo linfo);
diff --git a/src/latex.c b/src/latex.c
index 486d208..23e798b 100644
--- a/src/latex.c
+++ b/src/latex.c
@@ -117,12 +117,12 @@ latexTermPrint (Term term, Termlist highlight)
     {
       if (inTermlist (highlight, term))
 	printf ("\\mathbf{");
-      symbolPrint (TermSymb(term));
+      symbolPrint (TermSymb (term));
       if (realTermVariable (term))
 	printf ("V");
-      if (TermRunid(term) >= 0)
+      if (TermRunid (term) >= 0)
 	{
-	  printf ("\\sharp%i", TermRunid(term));
+	  printf ("\\sharp%i", TermRunid (term));
 	}
       if (term->subst != NULL)
 	{
@@ -141,22 +141,22 @@ latexTermPrint (Term term, Termlist highlight)
     }
   if (realTermEncrypt (term))
     {
-      if (isTermLeaf (TermKey(term))
-	  && inTermlist (TermKey(term)->stype, TERM_Function))
+      if (isTermLeaf (TermKey (term))
+	  && inTermlist (TermKey (term)->stype, TERM_Function))
 	{
 	  /* function application */
-	  latexTermPrint (TermKey(term), highlight);
+	  latexTermPrint (TermKey (term), highlight);
 	  printf ("(");
-	  latexTermTuplePrint (TermOp(term), highlight);
+	  latexTermTuplePrint (TermOp (term), highlight);
 	  printf (")");
 	}
       else
 	{
 	  /* normal encryption */
 	  printf ("\\{");
-	  latexTermTuplePrint (TermOp(term), highlight);
+	  latexTermTuplePrint (TermOp (term), highlight);
 	  printf ("\\}_{");
-	  latexTermPrint (TermKey(term), highlight);
+	  latexTermPrint (TermKey (term), highlight);
 	  printf ("}");
 	}
     }
@@ -180,9 +180,9 @@ latexTermTuplePrint (Term term, Termlist hl)
   while (realTermTuple (term))
     {
       // To remove any brackets, change this into latexTermTuplePrint.
-      latexTermPrint (TermOp1(term), hl);
+      latexTermPrint (TermOp1 (term), hl);
       printf (",");
-      term = deVar (TermOp2(term));
+      term = deVar (TermOp2 (term));
     }
   latexTermPrint (term, hl);
   return;
@@ -966,7 +966,7 @@ attackDisplayLatex (const System sys)
 		{
 		  /* detect whether it's really local to this run */
 		  Term t = deVar (tl->term);
-		  if (isTermLeaf (t) && TermRunid(t) == i)
+		  if (isTermLeaf (t) && TermRunid (t) == i)
 		    {
 		      if (first)
 			{
diff --git a/src/main.c b/src/main.c
index 3b767b5..8cbfaf0 100644
--- a/src/main.c
+++ b/src/main.c
@@ -771,15 +771,15 @@ timersPrint (const System sys)
       if (realTermTuple (cl_scan->label))
 	{
 	  /* modern version: claim label is tuple (protocname, label) */
-          /* first print protocol.role */
-	  termPrint (TermOp1(cl_scan->label));
+	  /* first print protocol.role */
+	  termPrint (TermOp1 (cl_scan->label));
 	  eprintf ("\t");
 	  termPrint (cl_scan->rolename);
 	  eprintf ("\t");
 	  /* second print event_label */
 	  termPrint (cl_scan->type);
 	  eprintf ("_");
-	  termPrint (TermOp2(cl_scan->label));
+	  termPrint (TermOp2 (cl_scan->label));
 	  eprintf ("\t");
 	}
       else
@@ -790,7 +790,7 @@ timersPrint (const System sys)
 	  termPrint (cl_scan->rolename);
 	  eprintf (" (");
 	  termPrint (cl_scan->label);
-          eprintf (")\t");
+	  eprintf (")\t");
 	}
       /* print counts etc. */
       eprintf ("found:\t");
diff --git a/src/match_clp.c b/src/match_clp.c
index fc51f07..7f38db8 100644
--- a/src/match_clp.c
+++ b/src/match_clp.c
@@ -60,11 +60,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
       cl = constraintlistDuplicate (solvecons);
       cl =
 	constraintlistAdd (cl,
-			   makeConstraint (TermOp1(deVar (activeco->term)),
+			   makeConstraint (TermOp1 (deVar (activeco->term)),
 					   activeco->know));
       cl =
 	constraintlistAdd (cl,
-			   makeConstraint (TermOp2(deVar (activeco->term)),
+			   makeConstraint (TermOp2 (deVar (activeco->term)),
 					   activeco->know));
       solvecons = cl;
       flag = solve (sp, solvecons) || flag;
@@ -192,11 +192,11 @@ solve (const struct solvepass sp, Constraintlist solvecons)
 	  cl = constraintlistDuplicate (oldcl);
 	  cl =
 	    constraintlistAdd (cl,
-			       makeConstraint (TermOp(activeco->term),
+			       makeConstraint (TermOp (activeco->term),
 					       activeco->know));
 	  cl =
 	    constraintlistAdd (cl,
-			       makeConstraint (TermKey(activeco->term),
+			       makeConstraint (TermKey (activeco->term),
 					       activeco->know));
 	  solvecons = cl;
 	  flag = solve (sp, solvecons) || flag;
@@ -368,8 +368,8 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
 	{
 	  /* tuple */
 	  tl2 = termlistShallow (tl->next);
-	  tl2 = termlistAdd (tl2, TermOp1(t));
-	  tl2 = termlistAdd (tl2, TermOp2(t));
+	  tl2 = termlistAdd (tl2, TermOp1 (t));
+	  tl2 = termlistAdd (tl2, TermOp2 (t));
 	  sendAdd_clp (sys, run, tl2);
 	  termlistDelete (tl2);
 	}
@@ -378,15 +378,15 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
 	  /* encrypt */
 	  Term invkey;
 
-	  invkey = inverseKey (sys->know->inverses, TermKey(t));
+	  invkey = inverseKey (sys->know->inverses, TermKey (t));
 	  if (!hasTermVariable (invkey))
 	    {
 	      /* simple case: no variable inside */
 	      knowledgeAddTerm (sys->know, t);
 	      tl2 = termlistShallow (tl->next);
 	      if (inKnowledge (sys->know, invkey)
-		  && hasTermVariable (TermOp(t)))
-		tl2 = termlistAdd (tl2, TermOp(t));
+		  && hasTermVariable (TermOp (t)))
+		tl2 = termlistAdd (tl2, TermOp (t));
 	      sendAdd_clp (sys, run, tl2);
 	      termlistDelete (tl2);
 	    }
@@ -418,7 +418,7 @@ sendAdd_clp (const System sys, const int run, const Termlist tl)
 	      sys->constraints = constraintlistAdd (clbuf, co);
 	      /* we _could_ explore first if this is solveable */
 	      knowledgeAddTerm (sys->know, t);
-	      tl2 = termlistAdd (tl2, TermOp(t));
+	      tl2 = termlistAdd (tl2, TermOp (t));
 	      sendAdd_clp (sys, run, tl2);
 
 	      termlistDelete (tl2);
diff --git a/src/mgu.c b/src/mgu.c
index a560741..d9e2891 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -183,14 +183,14 @@ termMguTerm (Term t1, Term t2)
     {
       Termlist tl1, tl2;
 
-      tl1 = termMguTerm (TermKey(t1), TermKey(t2));
+      tl1 = termMguTerm (TermKey (t1), TermKey (t2));
       if (tl1 == MGUFAIL)
 	{
 	  return MGUFAIL;
 	}
       else
 	{
-	  tl2 = termMguTerm (TermOp(t1), TermOp(t2));
+	  tl2 = termMguTerm (TermOp (t1), TermOp (t2));
 	  if (tl2 == MGUFAIL)
 	    {
 	      termlistSubstReset (tl1);
@@ -210,14 +210,14 @@ termMguTerm (Term t1, Term t2)
     {
       Termlist tl1, tl2;
 
-      tl1 = termMguTerm (TermOp1(t1), TermOp1(t2));
+      tl1 = termMguTerm (TermOp1 (t1), TermOp1 (t2));
       if (tl1 == MGUFAIL)
 	{
 	  return MGUFAIL;
 	}
       else
 	{
-	  tl2 = termMguTerm (TermOp2(t1), TermOp2(t2));
+	  tl2 = termMguTerm (TermOp2 (t1), TermOp2 (t2));
 	  if (tl2 == MGUFAIL)
 	    {
 	      termlistSubstReset (tl1);
@@ -251,8 +251,8 @@ termMguInTerm (Term t1, Term t2, int (*iterator) (Termlist))
       if (realTermTuple (t2))
 	{
 	  // t2 is a tuple, consider interm options as well.
-	  flag = flag && termMguInTerm (t1, TermOp1(t2), iterator);
-	  flag = flag && termMguInTerm (t1, TermOp2(t2), iterator);
+	  flag = flag && termMguInTerm (t1, TermOp1 (t2), iterator);
+	  flag = flag && termMguInTerm (t1, TermOp2 (t2), iterator);
 	}
       // simple clause or combined
       tl = termMguTerm (t1, t2);
@@ -300,10 +300,10 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
 	    {
 	      // 'simple' tuple
 	      flag =
-		flag && termMguSubTerm (t1, TermOp1(t2), iterator, inverses,
+		flag && termMguSubTerm (t1, TermOp1 (t2), iterator, inverses,
 					keylist);
 	      flag =
-		flag && termMguSubTerm (t1, TermOp2(t2), iterator, inverses,
+		flag && termMguSubTerm (t1, TermOp2 (t2), iterator, inverses,
 					keylist);
 	    }
 	  else
@@ -312,19 +312,20 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (Termlist, Termlist),
 	      // So, we need the key, and try to get the rest
 	      Term newkey;
 
-	      newkey = inverseKey (inverses, TermKey(t2));
+	      newkey = inverseKey (inverses, TermKey (t2));
 	      // We can never produce the TERM_Hidden key, thus, this is not a valid iteration.
 	      if (!isTermEqual (newkey, TERM_Hidden))
 		{
-	          Termlist keylist_new;
+		  Termlist keylist_new;
 
 		  keylist_new = termlistShallow (keylist);
 		  keylist_new = termlistAdd (keylist_new, newkey);
 
 		  // Recurse
 		  flag =
-		    flag && termMguSubTerm (t1, TermOp(t2), iterator, inverses,
-					    keylist_new);
+		    flag
+		    && termMguSubTerm (t1, TermOp (t2), iterator, inverses,
+				       keylist_new);
 
 		  termlistDelete (keylist_new);
 		}
diff --git a/src/modelchecker.c b/src/modelchecker.c
index 798803d..135917d 100644
--- a/src/modelchecker.c
+++ b/src/modelchecker.c
@@ -1147,7 +1147,7 @@ claimSecrecy (const System sys, const Term t)
   {
     t = deVar (t);
     if (isTermTuple (t))
-      return csScan (TermOp1(t)) && csScan (TermOp2(t));
+      return csScan (TermOp1 (t)) && csScan (TermOp2 (t));
     else
       return isTermSecret (sys, t);
   }
@@ -1171,8 +1171,8 @@ secrecyUnfolding (Term t, const Knowledge know)
 {
   t = deVar (t);
   if (isTermTuple (t))
-    return termlistConcat (secrecyUnfolding (TermOp1(t), know),
-			   secrecyUnfolding (TermOp2(t), know));
+    return termlistConcat (secrecyUnfolding (TermOp1 (t), know),
+			   secrecyUnfolding (TermOp2 (t), know));
   else
     {
       if (inKnowledge (know, t))
diff --git a/src/role.c b/src/role.c
index 1592d3f..6a8653c 100644
--- a/src/role.c
+++ b/src/role.c
@@ -61,7 +61,7 @@ roledefPrintGeneric (Roledef rd, int print_actor)
       if (protocolCount < 2 && realTermTuple (label))
 	{
 	  // Only one protocol, so we don't need to show the extra label info
-	  label = TermOp2(label);
+	  label = TermOp2 (label);
 	}
 
       //! Print latex/normal
@@ -84,8 +84,8 @@ roledefPrintGeneric (Roledef rd, int print_actor)
     {
       if (print_actor || rd->type == READ)
 	{
-          termPrint (rd->from);
-          eprintf (",");
+	  termPrint (rd->from);
+	  eprintf (",");
 	}
       if (rd->type == CLAIM)
 	eprintf (" ");
diff --git a/src/substitution.c b/src/substitution.c
index 53035c9..0cc21ee 100644
--- a/src/substitution.c
+++ b/src/substitution.c
@@ -64,14 +64,14 @@ termSubstitute (Term term, Substitution subs)
 	{
 	  if (isTermEncrypt (term))
 	    {
-	      return makeTermEncrypt (termSubstitute (TermOp(term), subs),
-				      termSubstitute (TermKey(term), subs));
+	      return makeTermEncrypt (termSubstitute (TermOp (term), subs),
+				      termSubstitute (TermKey (term), subs));
 	    }
 	  else
 	    {
 	      return
-		makeTermTuple (termSubstitute (TermOp1(term), subs),
-			       termSubstitute (TermOp2(term), subs));
+		makeTermTuple (termSubstitute (TermOp1 (term), subs),
+			       termSubstitute (TermOp2 (term), subs));
 	    }
 	}
       else
diff --git a/src/system.c b/src/system.c
index 4a23d78..2cc2524 100644
--- a/src/system.c
+++ b/src/system.c
@@ -563,7 +563,7 @@ create_new_local (const Term t, const int rid)
     {
       Term newt;
 
-      newt = makeTermType (t->type, TermSymb(t), rid);
+      newt = makeTermType (t->type, TermSymb (t), rid);
       newt->stype = t->stype;
 
       return newt;
@@ -667,7 +667,7 @@ roleInstanceArachne (const System sys, const Protocol protocol,
       if (realTermVariable (newt))
 	{
 	  // Make new var for this run
-	  newt = makeTermType (VARIABLE, TermSymb(newt), rid);
+	  newt = makeTermType (VARIABLE, TermSymb (newt), rid);
 	  artefacts = termlistAdd (artefacts, newt);
 	  newt->stype = oldt->stype;
 	  // Copy substitution
@@ -808,7 +808,7 @@ roleInstanceModelchecker (const System sys, const Protocol protocol,
 
 	  /* There is a TYPE constant in the parameter list.
 	   * Generate a new local variable for this run, with this type */
-	  newvar = makeTermType (VARIABLE, TermSymb(scanfrom->term), rid);
+	  newvar = makeTermType (VARIABLE, TermSymb (scanfrom->term), rid);
 	  artefacts = termlistAdd (artefacts, newvar);
 	  sys->variables = termlistAdd (sys->variables, newvar);
 	  newvar->stype = termlistAdd (NULL, scanto->term);
@@ -1200,7 +1200,7 @@ agentsOfRunPrint (const System sys, const int run)
       if (!isTermEqual (role, roles->term))
 	{
 	  if (notfirst)
-	      eprintf (", ");
+	    eprintf (", ");
 	  termPrint (roles->term);
 	  eprintf (":");
 	  termPrint (agentOfRunRole (sys, run, roles->term));
diff --git a/src/term.c b/src/term.c
index 28d1127..342595f 100644
--- a/src/term.c
+++ b/src/term.c
@@ -75,8 +75,8 @@ makeTermEncrypt (Term t1, Term t2)
   Term term = makeTerm ();
   term->type = ENCRYPT;
   term->stype = NULL;
-  TermOp(term) = t1;
-  TermKey(term) = t2;
+  TermOp (term) = t1;
+  TermKey (term) = t2;
   return term;
 }
 
@@ -111,8 +111,8 @@ makeTermTuple (Term t1, Term t2)
   tt = makeTerm ();
   tt->type = TUPLE;
   tt->stype = NULL;
-  TermOp1(tt) = t1;
-  TermOp2(tt) = t2;
+  TermOp1 (tt) = t1;
+  TermOp2 (tt) = t2;
   return tt;
 }
 
@@ -128,8 +128,8 @@ makeTermType (const int type, const Symbol symb, const int runid)
   term->type = type;
   term->stype = NULL;
   term->subst = NULL;
-  TermSymb(term) = symb;
-  TermRunid(term) = runid;
+  TermSymb (term) = symb;
+  TermRunid (term) = runid;
   return term;
 }
 
@@ -163,11 +163,11 @@ hasTermVariable (Term term)
   else
     {
       if (realTermTuple (term))
-	return (hasTermVariable (TermOp1(term))
-		|| hasTermVariable (TermOp2(term)));
+	return (hasTermVariable (TermOp1 (term))
+		|| hasTermVariable (TermOp2 (term)));
       else
-	return (hasTermVariable (TermOp(term))
-		|| hasTermVariable (TermKey(term)));
+	return (hasTermVariable (TermOp (term))
+		|| hasTermVariable (TermKey (term)));
     }
 }
 
@@ -206,8 +206,8 @@ isTermEqualFn (Term term1, Term term2)
     }
   if (realTermLeaf (term1))
     {
-      return (TermSymb(term1) == TermSymb(term2)
-	      && TermRunid(term1) == TermRunid(term2));
+      return (TermSymb (term1) == TermSymb (term2)
+	      && TermRunid (term1) == TermRunid (term2));
     }
   else
     {
@@ -218,15 +218,15 @@ isTermEqualFn (Term term1, Term term2)
 	  /* for optimization of encryption equality, we compare
 	     operator 2 first (we expect it to be a smaller term)
 	   */
-	  return (isTermEqualFn (TermKey(term1), TermKey(term2)) &&
-		  isTermEqualFn (TermOp(term1), TermOp(term2)));
+	  return (isTermEqualFn (TermKey (term1), TermKey (term2)) &&
+		  isTermEqualFn (TermOp (term1), TermOp (term2)));
 	}
       else
 	{
 	  /* tuple */
 
-	  return (isTermEqualFn (TermOp1(term1), TermOp1(term2)) &&
-		  isTermEqualFn (TermOp2(term1), TermOp2(term2)));
+	  return (isTermEqualFn (TermOp1 (term1), TermOp1 (term2)) &&
+		  isTermEqualFn (TermOp2 (term1), TermOp2 (term2)));
 	}
     }
 }
@@ -248,11 +248,11 @@ termSubTerm (Term t, Term tsub)
   if (realTermLeaf (t))
     return 0;
   if (realTermTuple (t))
-    return (termSubTerm (TermOp1(t), tsub)
-	    || termSubTerm (TermOp2(t), tsub));
+    return (termSubTerm (TermOp1 (t), tsub)
+	    || termSubTerm (TermOp2 (t), tsub));
   else
-    return (termSubTerm (TermOp(t), tsub)
-	    || termSubTerm (TermKey(t), tsub));
+    return (termSubTerm (TermOp (t), tsub)
+	    || termSubTerm (TermKey (t), tsub));
 }
 
 //! See if a term is an interm of another.
@@ -272,8 +272,7 @@ termInTerm (Term t, Term tsub)
   if (realTermLeaf (t))
     return 0;
   if (realTermTuple (t))
-    return (termInTerm (TermOp1(t), tsub)
-	    || termInTerm (TermOp2(t), tsub));
+    return (termInTerm (TermOp1 (t), tsub) || termInTerm (TermOp2 (t), tsub));
   else
     return 0;
 }
@@ -303,15 +302,15 @@ termPrint (Term term)
 #endif
   if (realTermLeaf (term))
     {
-      symbolPrint (TermSymb(term));
+      symbolPrint (TermSymb (term));
       if (term->type == VARIABLE)
 	eprintf ("V");
-      if (TermRunid(term) >= 0)
+      if (TermRunid (term) >= 0)
 	{
 	  if (globalLatex && globalError == 0)
-	    eprintf ("\\sharp%i", TermRunid(term));
+	    eprintf ("\\sharp%i", TermRunid (term));
 	  else
-	    eprintf ("#%i", TermRunid(term));
+	    eprintf ("#%i", TermRunid (term));
 	}
       if (term->subst != NULL)
 	{
@@ -331,13 +330,13 @@ termPrint (Term term)
     }
   if (realTermEncrypt (term))
     {
-      if (isTermLeaf (TermKey(term))
-	  && inTermlist (TermKey(term)->stype, TERM_Function))
+      if (isTermLeaf (TermKey (term))
+	  && inTermlist (TermKey (term)->stype, TERM_Function))
 	{
 	  /* function application */
-	  termPrint (TermKey(term));
+	  termPrint (TermKey (term));
 	  eprintf ("(");
-	  termTuplePrint (TermOp(term));
+	  termTuplePrint (TermOp (term));
 	  eprintf (")");
 	}
       else
@@ -346,17 +345,17 @@ termPrint (Term term)
 	  if (globalLatex)
 	    {
 	      eprintf ("\\{");
-	      termTuplePrint (TermOp(term));
+	      termTuplePrint (TermOp (term));
 	      eprintf ("\\}_{");
-	      termPrint (TermKey(term));
+	      termPrint (TermKey (term));
 	      eprintf ("}");
 	    }
 	  else
 	    {
 	      eprintf ("{");
-	      termTuplePrint (TermOp(term));
+	      termTuplePrint (TermOp (term));
 	      eprintf ("}");
-	      termPrint (TermKey(term));
+	      termPrint (TermKey (term));
 	    }
 	}
     }
@@ -380,9 +379,9 @@ termTuplePrint (Term term)
   while (realTermTuple (term))
     {
       // To remove any brackets, change this into termTuplePrint.
-      termPrint (TermOp1(term));
+      termPrint (TermOp1 (term));
       eprintf (",");
-      term = deVar (TermOp2(term));
+      term = deVar (TermOp2 (term));
     }
   termPrint (term);
   return;
@@ -409,13 +408,13 @@ termDuplicate (const Term term)
   memcpy (newterm, term, sizeof (struct term));
   if (realTermEncrypt (term))
     {
-      TermOp(newterm) = termDuplicate (TermOp(term));
-      TermKey(newterm) = termDuplicate (TermKey(term));
+      TermOp (newterm) = termDuplicate (TermOp (term));
+      TermKey (newterm) = termDuplicate (TermKey (term));
     }
   else
     {
-      TermOp1(newterm) = termDuplicate (TermOp1(term));
-      TermOp2(newterm) = termDuplicate (TermOp2(term));
+      TermOp1 (newterm) = termDuplicate (TermOp1 (term));
+      TermOp2 (newterm) = termDuplicate (TermOp2 (term));
     }
   return newterm;
 }
@@ -464,13 +463,13 @@ termDuplicateDeep (const Term term)
     {
       if (realTermEncrypt (term))
 	{
-	  TermOp(newterm) = termDuplicateDeep (TermOp(term));
-	  TermKey(newterm) = termDuplicateDeep (TermKey(term));
+	  TermOp (newterm) = termDuplicateDeep (TermOp (term));
+	  TermKey (newterm) = termDuplicateDeep (TermKey (term));
 	}
       else
 	{
-	  TermOp1(newterm) = termDuplicateDeep (TermOp1(term));
-	  TermOp2(newterm) = termDuplicateDeep (TermOp2(term));
+	  TermOp1 (newterm) = termDuplicateDeep (TermOp1 (term));
+	  TermOp2 (newterm) = termDuplicateDeep (TermOp2 (term));
 	}
     }
   return newterm;
@@ -497,13 +496,13 @@ termDuplicateUV (Term term)
   memcpy (newterm, term, sizeof (struct term));
   if (realTermEncrypt (term))
     {
-      TermOp(newterm) = termDuplicateUV (TermOp(term));
-      TermKey(newterm) = termDuplicateUV (TermKey(term));
+      TermOp (newterm) = termDuplicateUV (TermOp (term));
+      TermKey (newterm) = termDuplicateUV (TermKey (term));
     }
   else
     {
-      TermOp1(newterm) = termDuplicateUV (TermOp1(term));
-      TermOp2(newterm) = termDuplicateUV (TermOp2(term));
+      TermOp1 (newterm) = termDuplicateUV (TermOp1 (term));
+      TermOp2 (newterm) = termDuplicateUV (TermOp2 (term));
     }
   return newterm;
 }
@@ -534,13 +533,13 @@ realTermDuplicate (const Term term)
       newterm->type = term->type;
       if (realTermEncrypt (term))
 	{
-	  TermOp(newterm) = realTermDuplicate (TermOp(term));
-	  TermKey(newterm) = realTermDuplicate (TermKey(term));
+	  TermOp (newterm) = realTermDuplicate (TermOp (term));
+	  TermKey (newterm) = realTermDuplicate (TermKey (term));
 	}
       else
 	{
-	  TermOp1(newterm) = realTermDuplicate (TermOp1(term));
-	  TermOp2(newterm) = realTermDuplicate (TermOp2(term));
+	  TermOp1 (newterm) = realTermDuplicate (TermOp1 (term));
+	  TermOp2 (newterm) = realTermDuplicate (TermOp2 (term));
 	}
     }
   return newterm;
@@ -560,13 +559,13 @@ termDelete (const Term term)
     {
       if (realTermEncrypt (term))
 	{
-	  termDelete (TermOp(term));
-	  termDelete (TermKey(term));
+	  termDelete (TermOp (term));
+	  termDelete (TermKey (term));
 	}
       else
 	{
-	  termDelete (TermOp1(term));
-	  termDelete (TermOp2(term));
+	  termDelete (TermOp1 (term));
+	  termDelete (TermOp2 (term));
 	}
       memFree (term, sizeof (struct term));
     }
@@ -589,29 +588,29 @@ termNormalize (Term term)
 
   if (realTermEncrypt (term))
     {
-      termNormalize (TermOp(term));
-      termNormalize (TermKey(term));
+      termNormalize (TermOp (term));
+      termNormalize (TermKey (term));
     }
   else
     {
       /* normalize left hand first,both for tupling and for
          encryption */
-      termNormalize (TermOp1(term));
+      termNormalize (TermOp1 (term));
       /* check for ((x,y),z) construct */
-      if (realTermTuple (TermOp1(term)))
+      if (realTermTuple (TermOp1 (term)))
 	{
 	  /* temporarily store the old terms */
-	  Term tx = TermOp1(TermOp1(term));
-	  Term ty = TermOp2(TermOp1(term));
-	  Term tz = TermOp2(term);
+	  Term tx = TermOp1 (TermOp1 (term));
+	  Term ty = TermOp2 (TermOp1 (term));
+	  Term tz = TermOp2 (term);
 	  /* move node */
-	  TermOp2(term) = TermOp1(term);
+	  TermOp2 (term) = TermOp1 (term);
 	  /* construct (x,(y,z)) version */
-	  TermOp1(term) = tx;
-	  TermOp1(TermOp2(term)) = ty;
-	  TermOp2(TermOp2(term)) = tz;
+	  TermOp1 (term) = tx;
+	  TermOp1 (TermOp2 (term)) = ty;
+	  TermOp2 (TermOp2 (term)) = tz;
 	}
-      termNormalize (TermOp2(term));
+      termNormalize (TermOp2 (term));
     }
 }
 
@@ -629,12 +628,12 @@ termRunid (Term term, int runid)
   if (realTermLeaf (term))
     {
       /* leaf */
-      if (TermRunid(term) == runid)
+      if (TermRunid (term) == runid)
 	return term;
       else
 	{
 	  Term newt = termDuplicate (term);
-	  TermRunid(newt) = runid;
+	  TermRunid (newt) = runid;
 	  return newt;
 	}
     }
@@ -643,13 +642,13 @@ termRunid (Term term, int runid)
       /* anything else, recurse */
       if (realTermEncrypt (term))
 	{
-	  return makeTermEncrypt (termRunid (TermOp(term), runid),
-				  termRunid (TermKey(term), runid));
+	  return makeTermEncrypt (termRunid (TermOp (term), runid),
+				  termRunid (TermKey (term), runid));
 	}
       else
 	{
-	  return makeTermTuple (termRunid (TermOp1(term), runid),
-				termRunid (TermOp2(term), runid));
+	  return makeTermTuple (termRunid (TermOp1 (term), runid),
+				termRunid (TermOp2 (term), runid));
 	}
     }
 }
@@ -674,7 +673,7 @@ tupleCount (Term tt)
 	}
       else
 	{
-	  return (tupleCount (TermOp1(tt)) + tupleCount (TermOp2(tt)));
+	  return (tupleCount (TermOp1 (tt)) + tupleCount (TermOp2 (tt)));
 	}
     }
 }
@@ -710,16 +709,16 @@ tupleProject (Term tt, int n)
   else
     {
       /* there is a tuple to traverse */
-      int left = tupleCount (TermOp1(tt));
+      int left = tupleCount (TermOp1 (tt));
       if (n >= left)
 	{
 	  /* it's in the right hand side */
-	  return tupleProject (TermOp2(tt), n - left);
+	  return tupleProject (TermOp2 (tt), n - left);
 	}
       else
 	{
 	  /* left hand side */
-	  return tupleProject (TermOp1(tt), n);
+	  return tupleProject (TermOp1 (tt), n);
 	}
     }
 }
@@ -749,11 +748,11 @@ termSize (Term t)
     {
       if (realTermEncrypt (t))
 	{
-	  return 1 + termSize (TermOp(t)) + termSize (TermKey(t));
+	  return 1 + termSize (TermOp (t)) + termSize (TermKey (t));
 	}
       else
 	{
-	  return termSize (TermOp1(t)) + termSize (TermOp2(t));
+	  return termSize (TermOp1 (t)) + termSize (TermOp2 (t));
 	}
     }
 }
@@ -811,13 +810,13 @@ termDistance (Term t1, Term t2)
 	  if (isTermEncrypt (t1))
 	    {
 	      /* encryption */
-	      return (termDistance (TermOp(t1), TermOp(t2)) +
-		      termDistance (TermKey(t1), TermKey(t2))) / 2;
+	      return (termDistance (TermOp (t1), TermOp (t2)) +
+		      termDistance (TermKey (t1), TermKey (t2))) / 2;
 	    }
 	  else
 	    {
-	      return (termDistance (TermOp1(t1), TermOp1(t2)) +
-		      termDistance (TermOp2(t1), TermOp2(t2))) / 2;
+	      return (termDistance (TermOp1 (t1), TermOp1 (t2)) +
+		      termDistance (TermOp2 (t1), TermOp2 (t2))) / 2;
 	    }
 	}
     }
@@ -859,7 +858,7 @@ termOrder (Term t1, Term t2)
       /* compare names */
       int comp;
 
-      comp = strcmp (TermSymb(t1)->text, TermSymb(t2)->text);
+      comp = strcmp (TermSymb (t1)->text, TermSymb (t2)->text);
       if (comp != 0)
 	{
 	  /* names differ */
@@ -868,14 +867,14 @@ termOrder (Term t1, Term t2)
       else
 	{
 	  /* equal names, compare run identifiers */
-	  if (TermRunid(t1) == TermRunid(t2))
+	  if (TermRunid (t1) == TermRunid (t2))
 	    {
 	      error
 		("termOrder: two terms seem to be identical although local precondition says they aren't.");
 	    }
 	  else
 	    {
-	      if (TermRunid(t1) < TermRunid(t2))
+	      if (TermRunid (t1) < TermRunid (t2))
 		return -1;
 	      else
 		return 1;
@@ -889,13 +888,13 @@ termOrder (Term t1, Term t2)
 
       if (isTermEncrypt (t1))
 	{
-	  compL = termOrder (TermOp(t1), TermOp(t2));
-	  compR = termOrder (TermKey(t1), TermKey(t2));
+	  compL = termOrder (TermOp (t1), TermOp (t2));
+	  compR = termOrder (TermKey (t1), TermKey (t2));
 	}
       else
 	{
-	  compL = termOrder (TermOp1(t1), TermOp1(t2));
-	  compR = termOrder (TermOp2(t1), TermOp2(t2));
+	  compL = termOrder (TermOp1 (t1), TermOp1 (t2));
+	  compR = termOrder (TermOp2 (t1), TermOp2 (t2));
 	}
       if (compL != 0)
 	return compL;
@@ -931,10 +930,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
 	  // Left part
 	  if (realTermTuple (term))
 	    flag = flag
-	      && (term_iterate (TermOp1(term), leaf, nodel, nodem, noder));
+	      && (term_iterate (TermOp1 (term), leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
-	      && (term_iterate (TermOp(term), leaf, nodel, nodem, noder));
+	      && (term_iterate (TermOp (term), leaf, nodel, nodem, noder));
 
 	  if (nodem != NULL)
 	    flag = flag && nodem (term);
@@ -942,10 +941,10 @@ term_iterate (const Term term, int (*leaf) (), int (*nodel) (),
 	  // Right part
 	  if (realTermTuple (term))
 	    flag = flag
-	      && (term_iterate (TermOp2(term), leaf, nodel, nodem, noder));
+	      && (term_iterate (TermOp2 (term), leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
-	      && (term_iterate (TermKey(term), leaf, nodel, nodem, noder));
+	      && (term_iterate (TermKey (term), leaf, nodel, nodem, noder));
 
 	  if (noder != NULL)
 	    flag = flag && noder (term);
@@ -990,11 +989,11 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
 	    flag = flag
 	      &&
 	      (term_iterate_deVar
-	       (TermOp1(term), leaf, nodel, nodem, noder));
+	       (TermOp1 (term), leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
 	      &&
-	      (term_iterate_deVar (TermOp(term), leaf, nodel, nodem, noder));
+	      (term_iterate_deVar (TermOp (term), leaf, nodel, nodem, noder));
 
 	  if (nodem != NULL)
 	    flag = flag && nodem (term);
@@ -1004,11 +1003,12 @@ term_iterate_deVar (Term term, int (*leaf) (), int (*nodel) (),
 	    flag = flag
 	      &&
 	      (term_iterate_deVar
-	       (TermOp2(term), leaf, nodel, nodem, noder));
+	       (TermOp2 (term), leaf, nodel, nodem, noder));
 	  else
 	    flag = flag
 	      &&
-	      (term_iterate_deVar (TermKey(term), leaf, nodel, nodem, noder));
+	      (term_iterate_deVar
+	       (TermKey (term), leaf, nodel, nodem, noder));
 
 	  if (noder != NULL)
 	    flag = flag && noder (term);
@@ -1037,11 +1037,11 @@ term_iterate_leaves (const Term term, int (*func) ())
       else
 	{
 	  if (realTermTuple (term))
-	    return (term_iterate_leaves (TermOp1(term), func)
-		    && term_iterate_leaves (TermOp2(term), func));
+	    return (term_iterate_leaves (TermOp1 (term), func)
+		    && term_iterate_leaves (TermOp2 (term), func));
 	  else
-	    return (term_iterate_leaves (TermOp(term), func)
-		    && term_iterate_leaves (TermKey(term), func));
+	    return (term_iterate_leaves (TermOp (term), func)
+		    && term_iterate_leaves (TermKey (term), func));
 	}
     }
   return 1;
@@ -1078,32 +1078,32 @@ int
 term_encryption_level (const Term term)
 {
   int iter_maxencrypt (Term term)
-    {
-      term = deVar (term);
-      if (realTermLeaf (term))
-	{
-	  return 0;
-	}
-      else
-	{
-	  if (realTermTuple (term))
-	    {
-	      int l,r;
+  {
+    term = deVar (term);
+    if (realTermLeaf (term))
+      {
+	return 0;
+      }
+    else
+      {
+	if (realTermTuple (term))
+	  {
+	    int l, r;
 
-	      l = iter_maxencrypt (TermOp1(term));
-	      r = iter_maxencrypt (TermOp2(term));
-	      if (l>r)
-		  return l;
-	      else
-		  return r;
-	    }
-	  else
-	    {
-	      // encrypt
-	      return 1+iter_maxencrypt (TermOp(term));
-	    }
-	}
-    }
+	    l = iter_maxencrypt (TermOp1 (term));
+	    r = iter_maxencrypt (TermOp2 (term));
+	    if (l > r)
+	      return l;
+	    else
+	      return r;
+	  }
+	else
+	  {
+	    // encrypt
+	    return 1 + iter_maxencrypt (TermOp (term));
+	  }
+      }
+  }
 
   return iter_maxencrypt (term);
 }
@@ -1134,13 +1134,13 @@ term_constrain_level (const Term term)
       {
 	if (realTermTuple (t))
 	  {
-	    tcl_iterate (TermOp1(t));
-	    tcl_iterate (TermOp2(t));
+	    tcl_iterate (TermOp1 (t));
+	    tcl_iterate (TermOp2 (t));
 	  }
 	else
 	  {
-	    tcl_iterate (TermOp(t));
-	    tcl_iterate (TermKey(t));
+	    tcl_iterate (TermOp (t));
+	    tcl_iterate (TermKey (t));
 	  }
       }
   }
@@ -1184,7 +1184,7 @@ term_set_keylevels (const Term term)
 	Symbol sym;
 
 	// So, it occurs at 'level' as key. If that is less than known, store.
-	sym = TermSymb(t);
+	sym = TermSymb (t);
 	if (level < sym->keylevel)
 	  {
 	    // New minimum level
@@ -1195,13 +1195,13 @@ term_set_keylevels (const Term term)
       {
 	if (realTermTuple (t))
 	  {
-	    scan_levels (level, TermOp1(t));
-	    scan_levels (level, TermOp2(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 (level, TermOp (t));
+	    scan_levels ((level + 1), TermKey (t));
 	  }
       }
   }
@@ -1220,16 +1220,16 @@ termPrintDiff (Term t1, Term t2)
   t2 = deVar (t2);
 
   void termFromTo (Term t1, Term t2)
-    {
-      t1 = deVar (t1);
-      t2 = deVar (t2);
+  {
+    t1 = deVar (t1);
+    t2 = deVar (t2);
 
-      eprintf (" [");
-      termPrint (t1);
-      eprintf ("]->[");
-      termPrint (t2);
-      eprintf ("] ");
-    }
+    eprintf (" [");
+    termPrint (t1);
+    eprintf ("]->[");
+    termPrint (t2);
+    eprintf ("] ");
+  }
 
   if (isTermEqual (t1, t2))
     {
@@ -1241,7 +1241,7 @@ termPrintDiff (Term t1, Term t2)
       if (t1->type != t2->type)
 	{
 	  // Different types
-	  termFromTo (t1,t2);
+	  termFromTo (t1, t2);
 	}
       else
 	{
@@ -1257,31 +1257,33 @@ termPrintDiff (Term t1, Term t2)
 	      if (realTermEncrypt (t1))
 		{
 		  // Encryption
-		  if (isTermEqual (TermOp(t1), TermOp(t2)) || isTermEqual (TermKey(t1), TermKey(t2)))
+		  if (isTermEqual (TermOp (t1), TermOp (t2))
+		      || isTermEqual (TermKey (t1), TermKey (t2)))
 		    {
 		      eprintf ("{");
-		      termPrintDiff (TermOp(t1), TermOp(t2));
+		      termPrintDiff (TermOp (t1), TermOp (t2));
 		      eprintf ("}");
-		      termPrintDiff (TermKey(t1), TermKey(t2));
+		      termPrintDiff (TermKey (t1), TermKey (t2));
 		    }
 		  else
 		    {
-		      termFromTo (t1,t2);
+		      termFromTo (t1, t2);
 		    }
 		}
 	      else
 		{
 		  // Tupling
-		  if (isTermEqual (TermOp1(t1), TermOp1(t2)) || isTermEqual (TermOp2(t1), TermOp2(t2)))
+		  if (isTermEqual (TermOp1 (t1), TermOp1 (t2))
+		      || isTermEqual (TermOp2 (t1), TermOp2 (t2)))
 		    {
 		      eprintf ("(");
-		      termPrintDiff (TermOp1(t1), TermOp1(t2));
+		      termPrintDiff (TermOp1 (t1), TermOp1 (t2));
 		      eprintf (")");
-		      termPrintDiff (TermOp2(t1), TermOp2(t2));
+		      termPrintDiff (TermOp2 (t1), TermOp2 (t2));
 		    }
 		  else
 		    {
-		      termFromTo (t1,t2);
+		      termFromTo (t1, t2);
 		    }
 		}
 	    }
diff --git a/src/termlist.c b/src/termlist.c
index c3b7069..8d5fe42 100644
--- a/src/termlist.c
+++ b/src/termlist.c
@@ -412,12 +412,12 @@ termlistAddVariables (Termlist tl, Term t)
   else
     {
       if (isTermEncrypt (t))
-	return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
-				     TermKey(t));
+	return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
+				     TermKey (t));
       else
 	return
-	  termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
-				TermOp2(t));
+	  termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
+				TermOp2 (t));
     }
 }
 
@@ -455,12 +455,12 @@ termlistAddRealVariables (Termlist tl, Term t)
   else
     {
       if (realTermEncrypt (t))
-	return termlistAddVariables (termlistAddVariables (tl, TermOp(t)),
-				     TermKey(t));
+	return termlistAddVariables (termlistAddVariables (tl, TermOp (t)),
+				     TermKey (t));
       else
 	return
-	  termlistAddVariables (termlistAddVariables (tl, TermOp1(t)),
-				TermOp2(t));
+	  termlistAddVariables (termlistAddVariables (tl, TermOp1 (t)),
+				TermOp2 (t));
     }
 }
 
@@ -479,11 +479,11 @@ termlistAddBasic (Termlist tl, Term t)
   if (!isTermLeaf (t))
     {
       if (isTermEncrypt (t))
-	return termlistAddBasic (termlistAddBasic (tl, TermOp(t)),
-				 TermKey(t));
+	return termlistAddBasic (termlistAddBasic (tl, TermOp (t)),
+				 TermKey (t));
       else
-	return termlistAddBasic (termlistAddBasic (tl, TermOp1(t)),
-				 TermOp2(t));
+	return termlistAddBasic (termlistAddBasic (tl, TermOp1 (t)),
+				 TermOp2 (t));
     }
   else
     {
@@ -571,8 +571,8 @@ inverseKey (Termlist inverses, Term key)
       return termDuplicate (TERM_Hidden);
     }
   /* check for the special case first: when it is effectively a function application  */
-  if (isTermEncrypt (key) && isTermLeaf (TermKey(key))
-      && inTermlist (deVar (TermKey(key))->stype, TERM_Function))
+  if (isTermEncrypt (key) && isTermLeaf (TermKey (key))
+      && inTermlist (deVar (TermKey (key))->stype, TERM_Function))
     {
       /* we are scanning for functions */
       /* scan the list */
@@ -581,15 +581,15 @@ inverseKey (Termlist inverses, Term key)
       {
 	/* in: {op}kk, nk
 	 * out: {op'}nk */
-	return makeTermEncrypt (termDuplicate (TermOp(orig)),
+	return makeTermEncrypt (termDuplicate (TermOp (orig)),
 				termDuplicate (newk));
       }
       while (inverses != NULL && inverses->next != NULL)
 	{
 
-	  if (isTermEqual (TermKey(key), inverses->term))
+	  if (isTermEqual (TermKey (key), inverses->term))
 	    return funKey (key, inverses->next->term);
-	  if (isTermEqual (TermKey(key), inverses->next->term))
+	  if (isTermEqual (TermKey (key), inverses->next->term))
 	    return funKey (key, inverses->term);
 	  inverses = inverses->next->next;
 	}
@@ -645,13 +645,13 @@ termLocal (Term t, Termlist fromlist, Termlist tolist, const int runid)
       Term newt = termNodeDuplicate (t);
       if (realTermTuple (t))
 	{
-	  TermOp1(newt) = termLocal (TermOp1(t), fromlist, tolist, runid);
-	  TermOp2(newt) = termLocal (TermOp2(t), fromlist, tolist, runid);
+	  TermOp1 (newt) = termLocal (TermOp1 (t), fromlist, tolist, runid);
+	  TermOp2 (newt) = termLocal (TermOp2 (t), fromlist, tolist, runid);
 	}
       else
 	{
-	  TermOp(newt) = termLocal (TermOp(t), fromlist, tolist, runid);
-	  TermKey(newt) = termLocal (TermKey(t), fromlist, tolist, runid);
+	  TermOp (newt) = termLocal (TermOp (t), fromlist, tolist, runid);
+	  TermKey (newt) = termLocal (TermKey (t), fromlist, tolist, runid);
 	}
       return newt;
     }
diff --git a/src/warshall.c b/src/warshall.c
index 19c28b4..e131e0f 100644
--- a/src/warshall.c
+++ b/src/warshall.c
@@ -111,7 +111,8 @@ warshall (int *graph, int nodes)
 /**
  * Some crude algorithm I sketched on the blackboard.
  */
-int graph_ranks (int *graph, int *ranks, int nodes)
+int
+graph_ranks (int *graph, int *ranks, int nodes)
 {
   int i;
   int todo;
@@ -142,10 +143,11 @@ int graph_ranks (int *graph, int *ranks, int nodes)
 	      refn = 0;
 	      while (refn < nodes)
 		{
-		  if (ranks[refn] >= rank && graph[graph_index(refn, n)] != 0)
-		      refn = nodes+1;
+		  if (ranks[refn] >= rank
+		      && graph[graph_index (refn, n)] != 0)
+		    refn = nodes + 1;
 		  else
-		      refn++;
+		    refn++;
 		}
 	      if (refn == nodes)
 		{