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