tuned;
authorwenzelm
Wed Apr 27 14:11:37 2011 +0200 (2011-04-27)
changeset 424854faf82d12b19
parent 42484 2777a27506d0
child 42486 01b03a124b81
tuned;
src/Pure/conv.ML
     1.1 --- a/src/Pure/conv.ML	Wed Apr 27 13:21:12 2011 +0200
     1.2 +++ b/src/Pure/conv.ML	Wed Apr 27 14:11:37 2011 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4    (case Thm.term_of ct of
     1.5      Abs (x, _, _) =>
     1.6        let
     1.7 -        val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
     1.8 +        val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt;
     1.9          val (v, ct') = Thm.dest_abs (SOME u) ct;
    1.10          val eq = cv (v, ctxt') ct';
    1.11        in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end