--- 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"