changeset 60320 | e7c0ca878120 |
parent 60319 | 127c2f00ca94 |
child 60323 | 9b3b812e6957 |
--- 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