diff -r 2af982715e5c -r 03ce2b2a29a2 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
+++ b/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
@@ -12,7 +12,7 @@
 setup {* Reify_Data.setup *}
 
 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
-  by (blast intro: ext)
+  by blast
 
 use "reflection.ML"