# HG changeset patch
# User wenzelm
# Date 1369591427 -7200
# Node ID d5fa8134332247a46f3a86938ff8a0edae165f41
# Parent  ba6b2876ef5ae2a13f963901dcc2be87ee787d36
more robust variant_free: avoid clash with consts name space (e.g. consts "x", "xa", etc.);

diff -r ba6b2876ef5a -r d5fa81343322 src/HOL/Tools/case_translation.ML
--- a/src/HOL/Tools/case_translation.ML	Sun May 26 19:29:15 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Sun May 26 20:03:47 2013 +0200
@@ -107,6 +107,10 @@
         val consts = Proof_Context.consts_of ctxt;
         fun is_const s = can (Consts.the_constraint consts) (Consts.intern consts s);
 
+        fun variant_free x used =
+          let val (x', used') = Name.variant x used
+          in if is_const x' then variant_free x' used' else (x', used') end;
+
         fun abs p tTs t =
           Syntax.const @{const_syntax case_abs} $
             fold constrain_Abs tTs (absfree p t);
@@ -120,7 +124,7 @@
 
         (* replace occurrences of dummy_pattern by distinct variables *)
         fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
-              let val (x, used') = Name.variant "x" used
+              let val (x, used') = variant_free "x" used
               in (Free (x, T), used') end
           | replace_dummies (t $ u) used =
               let