src/HOL/Library/reflection.ML
changeset 46510 696f3fec3f83
parent 45403 7a0b8debef77
child 46763 aa9f5c3bcd4c
     1.1 --- a/src/HOL/Library/reflection.ML	Thu Feb 16 22:54:40 2012 +0100
     1.2 +++ b/src/HOL/Library/reflection.ML	Thu Feb 16 23:07:01 2012 +0100
     1.3 @@ -16,10 +16,6 @@
     1.4  structure Reflection : REFLECTION =
     1.5  struct
     1.6  
     1.7 -val ext2 = @{thm ext2};
     1.8 -val nth_Cons_0 = @{thm nth_Cons_0};
     1.9 -val nth_Cons_Suc = @{thm nth_Cons_Suc};
    1.10 -
    1.11    (* Make a congruence rule out of a defining equation for the interpretation *)
    1.12    (* th is one defining equation of f, i.e.
    1.13       th is "f (Cp ?t1 ... ?tn) = P(f ?t1, .., f ?tn)" *)
    1.14 @@ -59,7 +55,7 @@
    1.15  
    1.16     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)))
    1.17       | mk_def (t, v) = HOLogic.mk_Trueprop (HOLogic.mk_eq (v, t))
    1.18 -   fun tryext x = (x RS ext2 handle THM _ =>  x)
    1.19 +   fun tryext x = (x RS @{lemma "(\<forall>x. f x = g x) \<Longrightarrow> f = g" by blast} handle THM _ =>  x)
    1.20     val cong =
    1.21      (Goal.prove ctxt'' [] (map mk_def env)
    1.22        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
    1.23 @@ -295,7 +291,8 @@
    1.24      val th = trytrans corr_thms
    1.25      val ft = (Thm.dest_arg1 o Thm.dest_arg o Thm.dest_arg o cprop_of) th
    1.26      val rth = conv ft
    1.27 -  in simplify (HOL_basic_ss addsimps raw_eqs addsimps [nth_Cons_0, nth_Cons_Suc])
    1.28 +  in
    1.29 +    simplify (HOL_basic_ss addsimps raw_eqs addsimps @{thms nth_Cons_0 nth_Cons_Suc})
    1.30               (simplify (HOL_basic_ss addsimps [rth]) th)
    1.31    end
    1.32