--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 08:49:26 2010 +0100
@@ -78,7 +78,7 @@
Const (atom_name "" T j, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
(* term * term -> order *)
@@ -446,7 +446,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name Algebras.divide},
+ | n2 => Const (@{const_name Rings.divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\