src/HOL/Library/reflection.ML

   val genreif : Proof.context -> thm list -> term -> thm
 end;
 
 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)" *)
   (* Cp is a constructor pattern and P is a pattern *)

                                SOME v => v
                              | NONE => t)
 
    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)))
       (fn {context, prems, ...} =>
         Local_Defs.unfold_tac context (map tryext prems) THEN rtac th' 1)) RS sym

       | trytrans (th::ths) =
            (FWD trans [reifth, th RS sym] handle THM _ => trytrans ths)
     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
 
 fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
   let