changeset 33640 | 0d82107dc07a |
parent 32960 | 69916a850301 |
--- a/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:48 2009 +0100 +++ b/src/HOL/Lambda/StrongNorm.thy Thu Nov 12 17:21:51 2009 +0100 @@ -186,7 +186,7 @@ by (rule typing.App) qed with Cons True show ?thesis - by (simp add: map_compose [symmetric] comp_def) + by (simp add: comp_def) qed next case False