tuned;
authorwenzelm
Sun, 31 May 2015 00:11:12 +0200
changeset 60320 e7c0ca878120
parent 60319 127c2f00ca94
child 60321 42079156c5aa
tuned;
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