src/Pure/conv.ML
changeset 26130 03a7cfed5e9e
parent 24834 5684cbf8c895
child 26571 114da911bc41
     1.1 --- a/src/Pure/conv.ML	Mon Feb 25 16:31:17 2008 +0100
     1.2 +++ b/src/Pure/conv.ML	Mon Feb 25 16:31:18 2008 +0100
     1.3 @@ -76,7 +76,7 @@
     1.4        let
     1.5          val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt;
     1.6          val (v, ct') = Thm.dest_abs (SOME u) ct;
     1.7 -        val eq = (cv ctxt') ct';
     1.8 +        val eq = cv ctxt' ct';
     1.9        in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end
    1.10    | _ => raise CTERM ("abs_conv", [ct]));
    1.11