# HG changeset patch
# User wenzelm
# Date 1203953478 -3600
# Node ID 03a7cfed5e9ed0ee086f8d37af68632310c00b51
# Parent  14f6dbb195c4169fda9b1ae6e1666f959db2fae8
tuned;

diff -r 14f6dbb195c4 -r 03a7cfed5e9e src/Pure/conv.ML
--- a/src/Pure/conv.ML	Mon Feb 25 16:31:17 2008 +0100
+++ b/src/Pure/conv.ML	Mon Feb 25 16:31:18 2008 +0100
@@ -76,7 +76,7 @@
       let
         val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
         val (v, ct') = Thm.dest_abs (SOME u) ct;
-        val eq = (cv ctxt') ct';
+        val eq = cv ctxt' ct';
       in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
   | _ => raise CTERM ("abs_conv", [ct]));