diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index ecfc2cfc6..73db95249 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -23,6 +23,7 @@
 #include "config.h"
 #include "atomic_prop.hh"
 #include "visitor.hh"
+#include <cstddef>
 #include <cassert>
 #include <ostream>
 
@@ -67,10 +68,9 @@ namespace spot
     atomic_prop::~atomic_prop()
     {
       // Get this instance out of the instance map.
-      pair p(name(), &env());
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(name(), &env()));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
     }
 
     std::string
@@ -90,10 +90,8 @@ namespace spot
     const atomic_prop*
     atomic_prop::instance(const std::string& name, environment& env)
     {
-      pair p(name, &env);
       const atomic_prop* ap;
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(name, &env), nullptr));
       if (!ires.second)
 	ap = ires.first->second;
       else
@@ -111,13 +109,10 @@ namespace spot
     std::ostream&
     atomic_prop::dump_instances(std::ostream& os)
     {
-
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = " << i->second->ref_count_()
-	     << " * atomic_prop(" << i->first.first << ", "
-	     << i->first.second->name() << ")" << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = " << i.second->ref_count_()
+	   << " * atomic_prop(" << i.first.first << ", "
+	   << i.first.second->name() << ")" << std::endl;
       return os;
     }
 
diff --git a/src/ltlast/atomic_prop.hh b/src/ltlast/atomic_prop.hh
index 4282427c4..10744f116 100644
--- a/src/ltlast/atomic_prop.hh
+++ b/src/ltlast/atomic_prop.hh
@@ -72,8 +72,8 @@ namespace spot
       atomic_prop(const std::string& name, environment& env);
       virtual ~atomic_prop();
 
-      typedef std::pair<std::string, environment*> pair;
-      typedef std::map<pair, const atomic_prop*> map;
+      typedef std::pair<std::string, environment*> key;
+      typedef std::map<key, const atomic_prop*> map;
       static map instances;
 
     private:
diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc
index 3f628c3bf..fcc7930a1 100644
--- a/src/ltlast/automatop.cc
+++ b/src/ltlast/automatop.cc
@@ -19,6 +19,7 @@
 
 #include "config.h"
 #include <iostream>
+#include <cstddef>
 #include "automatop.hh"
 #include "nfa.hh"
 #include "visitor.hh"
@@ -60,10 +61,9 @@ namespace spot
     automatop::~automatop()
     {
       // Get this instance out of the instance map.
-      triplet p(std::make_pair(get_nfa(), negated_), children_);
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(get_nfa(), negated_, children_));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
 
       // Dereference children.
       unsigned s = size();
@@ -97,11 +97,10 @@ namespace spot
     const automatop*
     automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
     {
-      assert(nfa != 0);
-      triplet p(std::make_pair(nfa, negated), v);
+      assert(nfa);
       const automatop* res;
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(nfa, negated, v),
+						  nullptr));
       if (!ires.second)
 	{
 	  // The instance already exists.
@@ -127,13 +126,11 @@ namespace spot
     std::ostream&
     automatop::dump_instances(std::ostream& os)
     {
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = "
-	     << i->second->ref_count_() << " * "
-	     << i->second->dump()
-	     << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = "
+	   << i.second->ref_count_() << " * "
+	   << i.second->dump()
+	   << std::endl;
       return os;
     }
   }
diff --git a/src/ltlast/automatop.hh b/src/ltlast/automatop.hh
index eaeac3835..3b27f7854 100644
--- a/src/ltlast/automatop.hh
+++ b/src/ltlast/automatop.hh
@@ -24,6 +24,7 @@
 
 # include "refformula.hh"
 # include <vector>
+# include <tuple>
 # include <iosfwd>
 # include <map>
 # include "nfa.hh"
@@ -89,21 +90,21 @@ namespace spot
 
 
     protected:
-      typedef std::pair<std::pair<nfa::ptr, bool>, vec*> triplet;
+      typedef std::tuple<nfa::ptr, bool, vec*> key;
       /// Comparison functor used internally by ltl::automatop.
       struct tripletcmp
       {
 	bool
-	operator()(const triplet& p1, const triplet& p2) const
+	operator()(const key& p1, const key& p2) const
 	{
-	  if (p1.first.first != p2.first.first)
-	    return p1.first.first < p2.first.first;
-	  if (p1.first.second != p2.first.second)
-	    return p1.first.second < p2.first.second;
-	  return *p1.second < *p2.second;
+	  if (std::get<0>(p1) != std::get<0>(p2))
+	    return std::get<0>(p1) < std::get<0>(p2);
+	  if (std::get<1>(p1) != std::get<1>(p2))
+	    return std::get<1>(p1) < std::get<1>(p2);
+	  return *std::get<2>(p1) < *std::get<2>(p2);
 	}
       };
-      typedef std::map<triplet, const automatop*, tripletcmp> map;
+      typedef std::map<key, const automatop*> map;
       static map instances;
 
       automatop(const nfa::ptr, vec* v, bool negated);
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index e2faf9031..d4400b037 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -22,6 +22,7 @@
 
 #include "config.h"
 #include <cassert>
+#include <cstddef>
 #include <utility>
 #include "binop.hh"
 #include "unop.hh"
@@ -250,11 +251,9 @@ namespace spot
     binop::~binop()
     {
       // Get this instance out of the instance map.
-      pairf pf(first(), second());
-      pair p(op(), pf);
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(op(), first(), second()));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
 
       // Dereference children.
       first()->destroy();
@@ -506,12 +505,9 @@ namespace spot
 	  break;
 	}
 
-      pairf pf(first, second);
-      pair p(op, pf);
-
       const binop* res;
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(op, first, second),
+						  nullptr));
       if (!ires.second)
 	{
 	  // This instance already exists.
@@ -536,15 +532,12 @@ namespace spot
     std::ostream&
     binop::dump_instances(std::ostream& os)
     {
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = "
-	     << i->second->ref_count_() << " * "
-	     << i->second->dump()
-	     << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = "
+	   << i.second->ref_count_() << " * "
+	   << i.second->dump()
+	   << std::endl;
       return os;
-
     }
 
 
diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh
index 21b69bc0c..a88c2dfdf 100644
--- a/src/ltlast/binop.hh
+++ b/src/ltlast/binop.hh
@@ -31,6 +31,7 @@
 #include "refformula.hh"
 #include <map>
 #include <iosfwd>
+#include <tuple>
 
 namespace spot
 {
@@ -142,9 +143,8 @@ namespace spot
       static std::ostream& dump_instances(std::ostream& os);
 
     protected:
-      typedef std::pair<const formula*, const formula*> pairf;
-      typedef std::pair<type, pairf> pair;
-      typedef std::map<pair, const binop*> map;
+      typedef std::tuple<type, const formula*, const formula*> key;
+      typedef std::map<key, const binop*> map;
       static map instances;
 
       binop(type op, const formula* first, const formula* second);
diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index c5bb78491..2a43c4306 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -66,15 +66,14 @@ namespace spot
 
     bunop::~bunop()
     {
-      // one_star_ should never get delete.  Otherwise, that means
-      // is has been destroyed too much, or not cloned enough.
+      // one_star_ should never get deleted.  Otherwise, that means it
+      // has been destroyed too much, or not cloned enough.
       assert(this != one_star_);
 
       // Get this instance out of the instance map.
-      pair p(pairo(op(), child()), pairu(min_, max_));
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(op(), child(), min_, max_));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
 
       // Dereference child.
       child()->destroy();
@@ -239,11 +238,9 @@ namespace spot
 	  }
 	}
 
-      pair p(pairo(op, child), pairu(min, max));
-
       const formula* res;
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(op, child, min, max),
+						  nullptr));
       if (!ires.second)
 	{
 	  // This instance already exists.
@@ -303,13 +300,11 @@ namespace spot
     std::ostream&
     bunop::dump_instances(std::ostream& os)
     {
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = "
-	     << i->second->ref_count_() << " * "
-	     << i->second->dump()
-	     << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = "
+	   << i.second->ref_count_() << " * "
+	   << i.second->dump()
+	   << std::endl;
       return os;
     }
 
diff --git a/src/ltlast/bunop.hh b/src/ltlast/bunop.hh
index f37b2bc15..75cbb086b 100644
--- a/src/ltlast/bunop.hh
+++ b/src/ltlast/bunop.hh
@@ -25,6 +25,7 @@
 #include "refformula.hh"
 #include <map>
 #include <iosfwd>
+#include <tuple>
 #include "constant.hh"
 
 namespace spot
@@ -140,10 +141,8 @@ namespace spot
       }
 
     protected:
-      typedef std::pair<unsigned, unsigned> pairu;
-      typedef std::pair<type, const formula*> pairo;
-      typedef std::pair<pairo, pairu> pair;
-      typedef std::map<pair, const bunop*> map;
+      typedef std::tuple<type, const formula*, unsigned, unsigned> key;
+      typedef std::map<key, const bunop*> map;
       static map instances;
 
       bunop(type op, const formula* child, unsigned min, unsigned max);
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index 77ada7672..c5fdcacf9 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -21,6 +21,7 @@
 // along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
 #include "config.h"
+#include <cstddef>
 #include <cassert>
 #include <utility>
 #include <algorithm>
@@ -94,10 +95,9 @@ namespace spot
     multop::~multop()
     {
       // Get this instance out of the instance map.
-      pair p(op(), children_);
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(op(), children_));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
 
       // Dereference children.
       unsigned s = size();
@@ -593,19 +593,16 @@ namespace spot
 	  // to ensure that [*0] is not accepted.
 	  v->insert(v->begin(), constant::true_instance());
 	}
-      // The hash key.
-      pair p(op, v);
 
       const multop* res;
-      // Insert the key p with the dummy value 0 just
+      // Insert the key with the dummy nullptr just
       // to check if p already exists.
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(op, v), nullptr));
       if (!ires.second)
 	{
 	  // The instance did already exists.  Free v.
-	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
-	    (*vi)->destroy();
+	  for (auto f: *v)
+	    f->destroy();
 	  delete v;
 	  res = ires.first->second;
 	}
@@ -636,13 +633,11 @@ namespace spot
     std::ostream&
     multop::dump_instances(std::ostream& os)
     {
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = "
-	     << i->second->ref_count_() << " * "
-	     << i->second->dump()
-	     << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = "
+	   << i.second->ref_count_() << " * "
+	   << i.second->dump()
+	   << std::endl;
       return os;
     }
 
diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh
index a2a970964..ddeefe970 100644
--- a/src/ltlast/multop.hh
+++ b/src/ltlast/multop.hh
@@ -181,19 +181,19 @@ namespace spot
       static std::ostream& dump_instances(std::ostream& os);
 
     protected:
-      typedef std::pair<type, vec*> pair;
+      typedef std::pair<type, vec*> key;
       /// Comparison functor used internally by ltl::multop.
       struct paircmp
       {
 	bool
-	operator()(const pair& p1, const pair& p2) const
+	operator()(const key& p1, const key& p2) const
 	{
 	  if (p1.first != p2.first)
 	    return p1.first < p2.first;
 	  return *p1.second < *p2.second;
 	}
       };
-      typedef std::map<pair, const multop*, paircmp> map;
+      typedef std::map<key, const multop*, paircmp> map;
       static map instances;
 
       multop(type op, vec* v);
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 49e523413..3a91d7e5c 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -24,6 +24,7 @@
 #include "unop.hh"
 #include "visitor.hh"
 #include <cassert>
+#include <cstddef>
 #include <iostream>
 #include "constant.hh"
 #include "atomic_prop.hh"
@@ -146,10 +147,9 @@ namespace spot
     unop::~unop()
     {
       // Get this instance out of the instance map.
-      pair p(op(), child());
-      map::iterator i = instances.find(p);
-      assert (i != instances.end());
-      instances.erase(i);
+      size_t c = instances.erase(key(op(), child()));
+      assert(c == 1);
+      (void) c;			// For the NDEBUG case.
 
       // Dereference child.
       child()->destroy();
@@ -302,10 +302,7 @@ namespace spot
 	}
 
       const unop* res;
-      pair p(op, child);
-
-      std::pair<map::iterator, bool> ires =
-	instances.insert(map::value_type(p, 0));
+      auto ires = instances.insert(std::make_pair(key(op, child), nullptr));
       if (!ires.second)
 	{
 	  // This instance already exists.
@@ -329,13 +326,11 @@ namespace spot
     std::ostream&
     unop::dump_instances(std::ostream& os)
     {
-      for (map::iterator i = instances.begin(); i != instances.end(); ++i)
-	{
-	  os << i->second << " = "
-	     << i->second->ref_count_() << " * "
-	     << i->second->dump()
-	     << std::endl;
-	}
+      for (const auto& i: instances)
+	os << i.second << " = "
+	   << i.second->ref_count_() << " * "
+	   << i.second->dump()
+	   << std::endl;
       return os;
     }
 
diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh
index c861f2595..c24eb951c 100644
--- a/src/ltlast/unop.hh
+++ b/src/ltlast/unop.hh
@@ -115,8 +115,8 @@ namespace spot
       static std::ostream& dump_instances(std::ostream& os);
 
     protected:
-      typedef std::pair<type, const formula*> pair;
-      typedef std::map<pair, const unop*> map;
+      typedef std::pair<type, const formula*> key;
+      typedef std::map<key, const unop*> map;
       static map instances;
 
       unop(type op, const formula* child);