--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 12 19:44:37 2010 +0100
@@ -88,7 +88,7 @@
Const (nth_atom_name pool "" T j k, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name 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 *)
@@ -459,7 +459,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name Rings.divide},
+ | n2 => Const (@{const_name divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
@@ -470,7 +470,7 @@
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
else if not for_auto andalso
- constr_s = @{const_name NonStd} then
+ constr_s = @{const_name Silly} then
Const (fst (dest_Const (the_single ts)), T)
else
list_comb (Const constr_x, ts)