From 036a56e360d667d70bad6d4c497420964cfc1acd Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Fri, 23 Jan 2015 17:09:17 +0000
Subject: [PATCH] DoC: remove another unused variable

---
 src/muz/rel/udoc_relation.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 23f3a55f6..c527a9dba 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -948,7 +948,6 @@ namespace datalog {
 #if 0
         udoc_plugin::join_fn   m_joiner;
 #endif
-        union_find_default_ctx union_ctx;
         bit_vector             m_to_delete; 
 
     public: