diff -r dcb321249aa9 -r 01b711328990 src/HOL/ex/Reflection.thy
--- a/src/HOL/ex/Reflection.thy	Wed Aug 09 18:41:42 2006 +0200
+++ b/src/HOL/ex/Reflection.thy	Mon Aug 14 11:13:50 2006 +0200
@@ -7,9 +7,13 @@
 
 theory Reflection
 imports Main
-uses "reflection.ML"
+uses ("reflection.ML")
 begin
 
+lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
+  by (blast intro: ext)
+use "reflection.ML"
+
 method_setup reify = {*
   fn src =>
     Method.syntax (Attrib.thms --