author | wenzelm |
Sun, 31 May 2015 00:11:12 +0200 | |
changeset 60320 | e7c0ca878120 |
parent 60319 | 127c2f00ca94 |
child 60321 | 42079156c5aa |
src/Pure/drule.ML | file | annotate | diff | comparison | revisions |
--- 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