src/HOL/Library/Reflection.thy
changeset 45966 03ce2b2a29a2
parent 42814 5af15f1e2ef6
child 46510 696f3fec3f83
--- 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"