src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 34974 18b41bba42b5
parent 34936 c4f04bee79f3
child 34982 7b8c366e34a2
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      Const (atom_name "" T j, T)
     1.5  
     1.6  (* term -> real *)
     1.7 -fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
     1.8 +fun extract_real_number (Const (@{const_name Algebras.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 @@ -434,7 +434,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 HOL.divide},
    1.17 +                                 | n2 => Const (@{const_name Algebras.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.term_\