src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35402 115a5a95710a
parent 35388 42d39948cace
child 35408 b48ab741683b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:56:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 27 20:57:08 2010 +0100
     1.3 @@ -283,7 +283,7 @@
     1.4      (* bool -> typ -> typ -> (term * term) list -> term *)
     1.5      fun make_set maybe_opt T1 T2 tps =
     1.6        let
     1.7 -        val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
     1.8 +        val empty_const = Const (@{const_abbrev Set.empty}, T1 --> T2)
     1.9          val insert_const = Const (@{const_name insert},
    1.10                                    T1 --> (T1 --> T2) --> T1 --> T2)
    1.11          (* (term * term) list -> term *)
    1.12 @@ -313,7 +313,7 @@
    1.13          val update_const = Const (@{const_name fun_upd},
    1.14                                    (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
    1.15          (* (term * term) list -> term *)
    1.16 -        fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
    1.17 +        fun aux' [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
    1.18            | aux' ((t1, t2) :: ps) =
    1.19              (case t2 of
    1.20                 Const (@{const_name None}, _) => aux' ps