# HG changeset patch
# User haftmann
# Date 1291214787 -3600
# Node ID b3489aa6b63f48ed4c2cd38047be308ea357990d
# Parent  3ad8a5925ba480d46396c153c5c9d65c76aba09e
use type constructor as name for variable

diff -r 3ad8a5925ba4 -r b3489aa6b63f src/HOL/Tools/type_mapper.ML
--- a/src/HOL/Tools/type_mapper.ML	Wed Dec 01 11:46:20 2010 +0100
+++ b/src/HOL/Tools/type_mapper.ML	Wed Dec 01 15:46:27 2010 +0100
@@ -100,7 +100,7 @@
     val T1 = Type (tyco, Ts1);
     val T2 = Type (tyco, Ts2);
     val T3 = Type (tyco, Ts3);
-    val x = Free (the_single (Name.invents nctxt "a" 1), T3);
+    val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3);
     val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
     val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
       if not is_contra then
@@ -124,7 +124,7 @@
       replicate (bool_num co + bool_num contra) (T --> T)
     val Ts' = maps mk_argT (Ts ~~ variances)
     val T = Type (tyco, Ts);
-    val x = Free ("a", T);
+    val x = Free (Long_Name.base_name tyco, T);
     val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
       map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
   in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;