src/HOL/Tools/Groebner_Basis/groebner.ML
changeset 35625 9c818cab0dd0
parent 35410 1ea89d2a1bd4
child 36700 9b85b9d74b83
     1.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -967,10 +967,11 @@
     1.4            (semiring_normalize_wrapper ctxt res)) form));
     1.5  
     1.6  fun ring_tac add_ths del_ths ctxt =
     1.7 -  ObjectLogic.full_atomize_tac
     1.8 -  THEN' asm_full_simp_tac (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
     1.9 +  Object_Logic.full_atomize_tac
    1.10 +  THEN' asm_full_simp_tac
    1.11 +    (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
    1.12    THEN' CSUBGOAL (fn (p, i) =>
    1.13 -    rtac (let val form = (ObjectLogic.dest_judgment p)
    1.14 +    rtac (let val form = Object_Logic.dest_judgment p
    1.15            in case get_ring_ideal_convs ctxt form of
    1.16             NONE => reflexive form
    1.17            | SOME thy => #ring_conv thy form
    1.18 @@ -1008,7 +1009,7 @@
    1.19     end
    1.20    in  
    1.21       clarify_tac @{claset} i 
    1.22 -     THEN ObjectLogic.full_atomize_tac i 
    1.23 +     THEN Object_Logic.full_atomize_tac i 
    1.24       THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i 
    1.25       THEN clarify_tac @{claset} i 
    1.26       THEN (REPEAT (CONVERSION (#unwind_conv thy) i))