diff -r 7ff7fdfbb9a0 -r 58e5b16cbd94 src/HOL/Library/Rewrite.thy --- a/src/HOL/Library/Rewrite.thy Mon Apr 13 00:59:17 2015 +0200 +++ b/src/HOL/Library/Rewrite.thy Mon Apr 13 10:21:35 2015 +0200 @@ -10,7 +10,7 @@ consts rewrite_HOLE :: "'a::{}" notation rewrite_HOLE ("HOLE") -notation rewrite_HOLE ("\") +notation rewrite_HOLE ("\") lemma eta_expand: fixes f :: "'a::{} \ 'b::{}"