gensym: slightly more obscure prefix descreases probability of name clash;
authorwenzelm
Sun, 08 Jul 2007 19:52:04 +0200
changeset 23656 4bdcb024e95d
parent 23655 d2d1138e0ddc
child 23657 2332c79f4dc8
gensym: slightly more obscure prefix descreases probability of name clash;
src/Pure/conv.ML
--- a/src/Pure/conv.ML	Sun Jul 08 19:51:58 2007 +0200
+++ b/src/Pure/conv.ML	Sun Jul 08 19:52:04 2007 +0200
@@ -86,7 +86,7 @@
   (case Thm.term_of ct of
     Abs (x, _, _) =>
       let
-        val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct;
+        val (v, ct') = Thm.dest_abs (SOME (gensym "gensym_abs_")) ct;
         val eq = cv ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));