# HG changeset patch
# User wenzelm
# Date 1433023872 -7200
# Node ID e7c0ca878120145dee156ee02aac05e617265c1a
# Parent  127c2f00ca94877d7f6bfce3da79256ba5a94a94
tuned;

diff -r 127c2f00ca94 -r e7c0ca878120 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat May 30 23:58:06 2015 +0200
+++ b/src/Pure/drule.ML	Sun May 31 00:11:12 2015 +0200
@@ -838,7 +838,7 @@
             val (xs', t') = rename xs t;
             val (xs'', u') = rename xs' u;
           in (xs'', t' $ u') end
-      | rename xs t = (xs, t);
+      | rename xs a = (xs, a);
   in
     (case rename xs (Thm.prop_of thm) of
       ([], prop') => Thm.renamed_prop prop' thm