src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35177 168041f24f80
parent 35086 92a8c9ea5aa7
child 35179 4b198af5beb5
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Feb 10 11:47:33 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 12 19:44:37 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 Rings.divide}, _) $ t1 $ t2) =
     1.8 +fun extract_real_number (Const (@{const_name 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 Rings.divide},
    1.17 +                                 | n2 => Const (@{const_name 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.\
    1.21 @@ -470,7 +470,7 @@
    1.22                             constr_s = @{const_name Quot}) then
    1.23                      Const (abs_name, constr_T) $ the_single ts
    1.24                    else if not for_auto andalso
    1.25 -                          constr_s = @{const_name NonStd} then
    1.26 +                          constr_s = @{const_name Silly} then
    1.27                      Const (fst (dest_Const (the_single ts)), T)
    1.28                    else
    1.29                      list_comb (Const constr_x, ts)