diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc
index 220b69d1c..e32677204 100644
--- a/src/ltlast/atomic_prop.cc
+++ b/src/ltlast/atomic_prop.cc
@@ -102,13 +102,13 @@ namespace spot
     atomic_prop::instance(const std::string& name, environment& env)
     {
       pair p(name, &env);
-      // FIXME: Use lower_bound, or a hash_map.
-      map::iterator i = instances.find(p);
       const atomic_prop* ap;
-      if (i != instances.end())
-	ap = i->second;
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
+	ap = ires.first->second;
       else
-	ap = instances[p] = new atomic_prop(name, env);
+	ap = ires.first->second = new atomic_prop(name, env);
       ap->clone();
       return ap;
     }
diff --git a/src/ltlast/automatop.cc b/src/ltlast/automatop.cc
index 4a93d50ab..68c4535bd 100644
--- a/src/ltlast/automatop.cc
+++ b/src/ltlast/automatop.cc
@@ -95,19 +95,20 @@ namespace spot
     {
       assert(nfa != 0);
       triplet p(std::make_pair(nfa, negated), v);
-      map::iterator i = instances.find(p);
       const automatop* res;
-      if (i != instances.end())
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
 	{
 	  // The instance already exists.
 	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
 	    (*vi)->destroy();
 	  delete v;
-	  res = i->second;
+	  res = ires.first->second;
 	}
       else
 	{
-	  res = instances[p] = new automatop(nfa, v, negated);
+	  res = ires.first->second = new automatop(nfa, v, negated);
 	}
       res->clone();
       return res;
diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc
index fb39c7e9f..50427299c 100644
--- a/src/ltlast/binop.cc
+++ b/src/ltlast/binop.cc
@@ -525,19 +525,20 @@ namespace spot
 
       pairf pf(first, second);
       pair p(op, pf);
-      // FIXME: Use lower_bound or hash_map.
-      map::iterator i = instances.find(p);
+
       const binop* res;
-      if (i != instances.end())
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
 	{
 	  // This instance already exists.
 	  first->destroy();
 	  second->destroy();
-	  res = i->second;
+	  res = ires.first->second;
 	}
       else
 	{
-	  res = instances[p] = new binop(op, first, second);
+	  res = ires.first->second = new binop(op, first, second);
 	}
       res->clone();
       return res;
diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc
index dbfb53155..1ba7f9cfe 100644
--- a/src/ltlast/bunop.cc
+++ b/src/ltlast/bunop.cc
@@ -262,14 +262,20 @@ namespace spot
 	}
 
       pair p(pairo(op, child), pairu(min, max));
-      map::iterator i = instances.find(p);
-      if (i != instances.end())
+
+      const formula* res;
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
 	{
 	  // This instance already exists.
 	  child->destroy();
-	  return i->second->clone();
+	  res = ires.first->second;
+	}
+      else
+	{
+	  res = ires.first->second = new bunop(op, child, min, max);
 	}
-      const bunop* res = instances[p] = new bunop(op, child, min, max);
       res->clone();
       return res;
     }
diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc
index bb1b459f4..30bdbd817 100644
--- a/src/ltlast/multop.cc
+++ b/src/ltlast/multop.cc
@@ -588,21 +588,22 @@ namespace spot
       pair p(op, v);
 
       const multop* res;
-      // FIXME: Use lower_bound or hash_map.
-      map::iterator i = instances.find(p);
-      if (i != instances.end())
+      // Insert the key p with the dummy value 0 just
+      // to check if p already exists.
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
 	{
-	  // The instance already exists.
+	  // The instance did already exists.  Free v.
 	  for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
 	    (*vi)->destroy();
 	  delete v;
-	  res = i->second;
+	  res = ires.first->second;
 	}
       else
 	{
-	  // This is the first instance of this formula.
-	  // Record the instance in the map,
-	  res = instances[p] = new multop(op, v);
+	  // The instance did not already exist. 
+	  res = ires.first->second = new multop(op, v);
 	}
       res->clone();
       return res;
diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc
index 72053a4f1..8717493f1 100644
--- a/src/ltlast/unop.cc
+++ b/src/ltlast/unop.cc
@@ -314,16 +314,18 @@ namespace spot
 
       const unop* res;
       pair p(op, child);
-      map::iterator i = instances.find(p);
-      if (i != instances.end())
+
+      std::pair<map::iterator, bool> ires =
+	instances.insert(map::value_type(p, 0));
+      if (!ires.second)
 	{
 	  // This instance already exists.
 	  child->destroy();
-	  res = i->second;
+	  res = ires.first->second;
 	}
       else
 	{
-	  res = instances[p] = new unop(op, child);
+	  res = ires.first->second = new unop(op, child);
 	}
       res->clone();
       return res;