# HG changeset patch
# User wenzelm
# Date 1303906297 -7200
# Node ID 4faf82d12b194b961f9ee1c681549e04b2ca78a2
# Parent  2777a27506d0d8a56f5df615e82e240e1be04ea9
tuned;

diff -r 2777a27506d0 -r 4faf82d12b19 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Wed Apr 27 13:21:12 2011 +0200
+++ b/src/Pure/conv.ML	Wed Apr 27 14:11:37 2011 +0200
@@ -93,7 +93,7 @@
   (case Thm.term_of ct of
     Abs (x, _, _) =>
       let
-        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
+        val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
         val (v, ct') = Thm.dest_abs (SOME u) ct;
         val eq = cv (v, ctxt') ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end