src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35086 92a8c9ea5aa7
parent 35076 cc19e2aef17e
parent 35084 e25eedfc15ce
child 35177 168041f24f80
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 00:51:54 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 08:54:56 2010 +0100
     1.3 @@ -88,7 +88,7 @@
     1.4      Const (nth_atom_name pool "" T j k, T)
     1.5  
     1.6  (* term -> real *)
     1.7 -fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
     1.8 +fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
     1.9      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
    1.10    | extract_real_number t = real (snd (HOLogic.dest_number t))
    1.11  (* term * term -> order *)
    1.12 @@ -459,7 +459,7 @@
    1.13                             0 => mk_num 0
    1.14                           | n1 => case HOLogic.dest_number t2 |> snd of
    1.15                                     1 => mk_num n1
    1.16 -                                 | n2 => Const (@{const_name Algebras.divide},
    1.17 +                                 | n2 => Const (@{const_name Rings.divide},
    1.18                                                  num_T --> num_T --> num_T)
    1.19                                           $ mk_num n1 $ mk_num n2)
    1.20                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.\