1.1 --- a/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.2 +++ b/src/HOL/Library/Reflection.thy	Sat Dec 24 15:53:09 2011 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  setup {* Reify_Data.setup *}
     1.5  
     1.6  lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
     1.7 -  by (blast intro: ext)
     1.8 +  by blast
     1.9  
    1.10  use "reflection.ML"
    1.11