diff --git a/src/TODO-trampolines.txt b/src/TODO-trampolines.txt
index e34f389..06a961b 100644
--- a/src/TODO-trampolines.txt
+++ b/src/TODO-trampolines.txt
@@ -2,7 +2,6 @@
 1  subtermUnify 		arachne.c +961
 1  term_iterate_open_leaves 	dotout.c +1790 		// Could be replaced by term_iterate_leaves
 3  unify 			mgu.c +233 ; mgu.c +247 ; mgu.c +281
-1  iterateLocalToOther 		prune_theorems.c +108
 
 term_iterate_leaves
   term_iterate_state_leaves
@@ -13,5 +12,4 @@ iterateTermOther is called using makeDepend and addOther
 subtermUnify is called using unifiesWithKeys
 term_iterate_open_leaves is called using addsubterms
 unify is called using unify_combine_enc and unify_combined_tup, and a callback using the keys list? (which propagates back to subtermunify data)
-iterateLocalToOther is called using checkTerm
 
diff --git a/src/prune_theorems.c b/src/prune_theorems.c
index 546f45d..54852d8 100644
--- a/src/prune_theorems.c
+++ b/src/prune_theorems.c
@@ -41,6 +41,58 @@ extern Protocol INTRUDER;
 extern int proofDepth;
 extern int max_encryption_level;
 
+//! checkTerm is a helper for the next function
+int
+checkTerm (const System sys, const Term t, const int r1)
+{
+  if (!isTermVariable (t))
+    {
+      int r2;
+      int e1, e2;
+
+      // t is a term from r2 that occurs in r1
+      r2 = TermRunid (t);
+      e1 = firstOccurrence (sys, r1, t, ANYEVENT);
+      if (e1 >= 0)
+	{
+	  if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
+	    {
+	      e2 = firstOccurrence (sys, r2, t, SEND);
+	      if (e2 >= 0)
+		{
+		  // thus, it should not be the case that e1 occurs before e2
+		  if (isDependEvent (r1, e1, r2, e2))
+		    {
+		      // That's not good!
+		      if (switches.output == PROOF)
+			{
+			  indentPrint ();
+			  eprintf ("Pruned because ordering for term ");
+			  termSubstPrint (t);
+			  eprintf
+			    (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
+			     r2, e2, r1, e1);
+			}
+		      return false;
+		    }
+		}
+	    }
+	}
+      else
+	{
+	  globalError++;
+	  eprintf ("error: term ");
+	  termSubstPrint (t);
+	  eprintf
+	    (" from run %i should occur in run %i, but it doesn't.\n", r2,
+	     r1);
+	  globalError--;
+	  error ("Abort");
+	}
+    }
+  return true;
+}
+
 
 //! Check locals occurrence
 /*
@@ -51,56 +103,6 @@ correctLocalOrder (const System sys)
 {
   int r1;
 
-  int checkTerm (Term t)
-  {
-    if (!isTermVariable (t))
-      {
-	int r2;
-	int e1, e2;
-
-	// t is a term from r2 that occurs in r1
-	r2 = TermRunid (t);
-	e1 = firstOccurrence (sys, r1, t, ANYEVENT);
-	if (e1 >= 0)
-	  {
-	    if (roledef_shift (sys->runs[r1].start, e1)->type == RECV)
-	      {
-		e2 = firstOccurrence (sys, r2, t, SEND);
-		if (e2 >= 0)
-		  {
-		    // thus, it should not be the case that e1 occurs before e2
-		    if (isDependEvent (r1, e1, r2, e2))
-		      {
-			// That's not good!
-			if (switches.output == PROOF)
-			  {
-			    indentPrint ();
-			    eprintf ("Pruned because ordering for term ");
-			    termSubstPrint (t);
-			    eprintf
-			      (" cannot be correct: the first send r%ii%i occurs after the receive r%ii%i.\n",
-			       r2, e2, r1, e1);
-			  }
-			return false;
-		      }
-		  }
-	      }
-	  }
-	else
-	  {
-	    globalError++;
-	    eprintf ("error: term ");
-	    termSubstPrint (t);
-	    eprintf
-	      (" from run %i should occur in run %i, but it doesn't.\n", r2,
-	       r1);
-	    globalError--;
-	    error ("Abort");
-	  }
-      }
-    return true;
-  }
-
   for (r1 = 0; r1 < sys->maxruns; r1++)
     {
       if (sys->runs[r1].protocol != INTRUDER)
diff --git a/src/system.c b/src/system.c
index 4fa2742..0632d48 100644
--- a/src/system.c
+++ b/src/system.c
@@ -1129,9 +1129,14 @@ iterateEventsType (const System sys, const int run, const int evtype,
 }
 
 // Iterate over all 'others': local variables of a run that are instantiated and contain some term of another run.
+/**
+ * Now incorporates "checkterm" required argument of myrun to the callback:
+ *
+ * It's now callback(conts Term,const int);
+ */
 int
 iterateLocalToOther (const System sys, const int myrun,
-		     int (*callback) (Term tlocal))
+		     int (*callback) (const System, const Term, const int))
 {
   Termlist tlo, tls;
   int flag;
@@ -1158,7 +1163,7 @@ iterateLocalToOther (const System sys, const int myrun,
   // now iterate over all of them
   for (tls = tlo; flag && (tls != NULL); tls = tls->next)
     {
-      if (!callback (tls->term))
+      if (!callback (sys, tls->term, myrun))
 	{
 	  flag = false;
 	}
diff --git a/src/system.h b/src/system.h
index 8e75bbb..4a6f708 100644
--- a/src/system.h
+++ b/src/system.h
@@ -199,7 +199,8 @@ int iterateAllEvents (const System sys,
 int iterateEventsType (const System sys, const int run, const int evtype,
 		       int (*callback) (Roledef rd, int ev));
 int iterateLocalToOther (const System sys, const int myrun,
-			 int (*callback) (Term t));
+			 int (*callback) (const System sys, const Term t,
+					  const int myrun));
 int iterateRoles (const System sys, int (*callback) (Protocol p, Role r));
 int firstOccurrence (const System sys, const int r, Term t, int evtype);
 Roledef eventRoledef (const System sys, const int run, const int ev);