# HG changeset patch
# User wenzelm
# Date 1329430021 -3600
# Node ID 696f3fec3f836218fa1fa0313069311af1f867bb
# Parent  c4b2ec379fdd448b5f91eb7ff156075094b6b5fd
more antiquotations;

diff -r c4b2ec379fdd -r 696f3fec3f83 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Thu Feb 16 22:54:40 2012 +0100
+++ b/src/HOL/Library/Reflection.thy	Thu Feb 16 23:07:01 2012 +0100
@@ -11,9 +11,6 @@
 
 setup {* Reify_Data.setup *}
 
-lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
-  by blast
-
 use "reflection.ML"
 
 method_setup reify = {*
diff -r c4b2ec379fdd -r 696f3fec3f83 src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Thu Feb 16 22:54:40 2012 +0100
+++ b/src/HOL/Library/reflection.ML	Thu Feb 16 23:07:01 2012 +0100
@@ -16,10 +16,6 @@
 structure Reflection : REFLECTION =
 struct
 
-val ext2 = @{thm ext2};
-val nth_Cons_0 = @{thm nth_Cons_0};
-val nth_Cons_Suc = @{thm nth_Cons_Suc};
-
   (* Make a congruence rule out of a defining equation for the interpretation *)
   (* th is one defining equation of f, i.e.
      th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
@@ -59,7 +55,7 @@
 
    fun mk_def (Abs(x,xT,t),v) = HOLogic.mk_Trueprop ((HOLogic.all_const xT)$ Abs(x,xT,HOLogic.mk_eq(v$(Bound 0), t)))
      | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
-   fun tryext x = (x RS ext2 handle THM _ =>  x)
+   fun tryext x = (x RS @{lemma "(\<forall>x. f x = g x) \<Longrightarrow> f = g" by blast} handle THM _ =>  x)
    val cong =
     (Goal.prove ctxt'' [] (map mk_def env)
       (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
@@ -295,7 +291,8 @@
     val th = trytrans corr_thms
     val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
     val rth = conv ft
-  in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
+  in
+    simplify (HOL_basic_ss addsimps raw_eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
              (simplify (HOL_basic_ss addsimps [rth]) th)
   end