diff --git a/src/util/fresh_name.cpp b/src/util/fresh_name.cpp
index 9905e14c22..ac4f1db8de 100644
--- a/src/util/fresh_name.cpp
+++ b/src/util/fresh_name.cpp
@@ -91,6 +91,20 @@ name_generator mk_fresh_name_generator_child() {
     return get_name_generator().mk_child();
 }
 
+fresh_name_scope::fresh_name_scope():
+    m_old(get_name_generator()) {
+    get_name_generator() = name_generator(*g_fresh);
+}
+
+fresh_name_scope::fresh_name_scope(name_generator const & g):
+    m_old(get_name_generator()) {
+    get_name_generator() = g;
+}
+
+fresh_name_scope::~fresh_name_scope() {
+    get_name_generator() = m_old;
+}
+
 void initialize_fresh_name() {
     g_fresh = new name("_fresh");
 }
diff --git a/src/util/fresh_name.h b/src/util/fresh_name.h
index 9556571074..fca5ec7f00 100644
--- a/src/util/fresh_name.h
+++ b/src/util/fresh_name.h
@@ -45,6 +45,14 @@ void set_fresh_name_generator(name_generator const & g);
    We use this operation to set the name_generator before we execute a task. */
 name_generator mk_fresh_name_generator_child();
 
+struct fresh_name_scope {
+    name_generator m_old;
+public:
+    fresh_name_scope();
+    fresh_name_scope(name_generator const & g);
+    ~fresh_name_scope();
+};
+
 void initialize_fresh_name();
 void finalize_fresh_name();
 }