src/HOL/Tools/semiring_normalizer.ML
changeset 44064 5bce8ff0d9ae
parent 40077 c8a9eaaa2f59
child 46497 89ccf66aa73d
     1.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Mon Aug 08 08:55:49 2011 -0700
     1.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Mon Aug 08 09:52:09 2011 -0700
     1.3 @@ -185,14 +185,14 @@
     1.4    let
     1.5      fun numeral_is_const ct =
     1.6        case term_of ct of
     1.7 -       Const (@{const_name Rings.divide},_) $ a $ b =>
     1.8 +       Const (@{const_name Fields.divide},_) $ a $ b =>
     1.9           can HOLogic.dest_number a andalso can HOLogic.dest_number b
    1.10 -     | Const (@{const_name Rings.inverse},_)$t => can HOLogic.dest_number t
    1.11 +     | Const (@{const_name Fields.inverse},_)$t => can HOLogic.dest_number t
    1.12       | t => can HOLogic.dest_number t
    1.13      fun dest_const ct = ((case term_of ct of
    1.14 -       Const (@{const_name Rings.divide},_) $ a $ b=>
    1.15 +       Const (@{const_name Fields.divide},_) $ a $ b=>
    1.16          Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    1.17 -     | Const (@{const_name Rings.inverse},_)$t => 
    1.18 +     | Const (@{const_name Fields.inverse},_)$t => 
    1.19                     Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    1.20       | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    1.21         handle TERM _ => error "ring_dest_const")