# HG changeset patch
# User desharna
# Date 1607611687 -3600
# Node ID d56a9267eb1a06c52c8b80757dd454325d2b73a3
# Parent  f231444e8f9d8fa2c3fdcf87b22aa42b8f92792c
generate unique variable names in tptp

diff -r f231444e8f9d -r d56a9267eb1a src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 10 13:49:49 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Dec 10 15:48:07 2020 +0100
@@ -1103,14 +1103,29 @@
 
 val unmangled_invert_const = invert_const o hd o unmangled_const_name
 
-fun eta_expand_iterm tm =
-  let
-    val T = domain_type (ityp_of tm)
-    val x = "CHANGEME"
-  in
-    IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
+fun free_vars_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars
+  | free_vars_iterm vars (IVar ((s, _), _)) = insert (op =) s vars
+  | free_vars_iterm vars (IApp (tm1, tm2)) =
+    union (op =) (free_vars_iterm vars tm1) (free_vars_iterm vars tm2)
+  | free_vars_iterm vars (IAbs (((s, _), _), tm)) = remove (op =) s (free_vars_iterm vars tm)
+
+fun generate_unique_name (gen : int -> 'a) (unique : 'a -> bool) (n : int) : 'a =
+  let val x = gen n in
+    if unique x then x else generate_unique_name gen unique (n + 1)
   end
 
+fun eta_expand_quantifier_body (tm as IAbs _) = tm
+  | eta_expand_quantifier_body tm =
+    let
+      val free_vars = free_vars_iterm [] tm
+      val x = generate_unique_name
+        (fn n => "X" ^ (if n = 0 then "" else string_of_int n))
+        (fn name => not (exists (fn y => name = y) free_vars)) 0
+      val T = domain_type (ityp_of tm)
+    in
+      IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
+    end
+
 fun introduce_proxies_in_iterm type_enc =
   let
     fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
@@ -1144,7 +1159,7 @@
             (case tm1' of
               IConst ((s, _), _, _) =>
               if s = tptp_ho_forall orelse s = tptp_ho_exists then
-                eta_expand_iterm tm2'
+                eta_expand_quantifier_body tm2'
               else
                 tm2'
             | _ => tm2')