src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -1431,7 +1431,7 @@
     1.4  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
     1.5  
     1.6  fun sos_tac print_cert prover ctxt =
     1.7 -  ObjectLogic.full_atomize_tac THEN'
     1.8 +  Object_Logic.full_atomize_tac THEN'
     1.9    elim_denom_tac ctxt THEN'
    1.10    core_sos_tac print_cert prover ctxt;
    1.11