diff --git a/xlp.ml b/xlp.ml
index 3c57290..0be7b64 100644
--- a/xlp.ml
+++ b/xlp.ml
@@ -375,9 +375,14 @@ let print_let oc (t,t',_,_) =
 
 let decl_term_abbrev oc t (k,ntvs,bs) =
   let n = "term"^string_of_int k in
-  if ntvs > 0 then raw_update_tvs_map n ntvs;
   string oc "symbol "; string oc n;
-  for i=0 to ntvs-1 do string oc " a"; int oc i done;
+  if ntvs > 0 then
+    begin
+      raw_update_tvs_map n ntvs; 
+      string oc " (a0";
+      for i=1 to ntvs-1 do string oc " a"; int oc i done;
+      string oc " : Set)"
+    end;
   let decl_var i b =
     string oc " (x"; int oc i; string oc ": El "; abbrev_typ oc b; char oc ')'
   in