src/Pure/conv.ML
changeset 23656 4bdcb024e95d
parent 23596 f8381a95c49c
child 24834 5684cbf8c895
     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]));