# HG changeset patch
# User wenzelm
# Date 1183917124 -7200
# Node ID 4bdcb024e95dd158ad5334a5ad98c58a4ebab1e6
# Parent  d2d1138e0ddcf7063dae968a84162b35ae524b01
gensym: slightly more obscure prefix descreases probability of name clash;

diff -r d2d1138e0ddc -r 4bdcb024e95d 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]));