author | wenzelm |
Sun, 08 Jul 2007 19:52:04 +0200 | |
changeset 23656 | 4bdcb024e95d |
parent 23655 | d2d1138e0ddc |
child 23657 | 2332c79f4dc8 |
src/Pure/conv.ML | file | annotate | diff | comparison | revisions |
--- 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]));