# HG changeset patch
# User blanchet
# Date 1282125824 -7200
# Node ID 54727b44e277c4e4ce7986c68b750be3217cad93
# Parent  ba8027440fb018b43a3781cb04260e428f2f4fd0
handle bound name conflicts gracefully in FOF translation

diff -r ba8027440fb0 -r 54727b44e277 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Aug 18 11:14:33 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Aug 18 12:03:44 2010 +0200
@@ -55,8 +55,10 @@
   let
     val do_term = combterm_from_term thy
     fun do_quant bs q s T t' =
-      do_formula ((s, T) :: bs) t'
-      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+      let val s = Name.variant (map fst bs) s in
+        do_formula ((s, T) :: bs) t'
+        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+      end
     and do_conn bs c t1 t2 =
       do_formula bs t1 ##>> do_formula bs t2
       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))