src/HOL/Groebner_Basis.thy
changeset 35410 1ea89d2a1bd4
parent 35216 7641e8d831d2
child 36305 dbe99291eb3c
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Feb 28 22:30:51 2010 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Feb 28 23:51:31 2010 +0100
     1.3 @@ -510,7 +510,7 @@
     1.4      let
     1.5        val z = instantiate_cterm ([(zT,T)],[]) zr
     1.6        val eq = instantiate_cterm ([(eqT,T)],[]) geq
     1.7 -      val th = Simplifier.rewrite (ss addsimps simp_thms)
     1.8 +      val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
     1.9             (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
    1.10                    (Thm.capply (Thm.capply eq t) z)))
    1.11      in equal_elim (symmetric th) TrueI
    1.12 @@ -640,7 +640,7 @@
    1.13  
    1.14  val comp_conv = (Simplifier.rewrite
    1.15  (HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"}
    1.16 -              addsimps ths addsimps simp_thms
    1.17 +              addsimps ths addsimps @{thms simp_thms}
    1.18                addsimprocs Numeral_Simprocs.field_cancel_numeral_factors
    1.19                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
    1.20                              ord_frac_simproc]