fixed Nitpick's typedef handling w.r.t. "set"
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03)
changeset 46088948bef826443
parent 46087 680edc162249
child 46089 d98eb715444d
fixed Nitpick's typedef handling w.r.t. "set"
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -1923,14 +1923,14 @@
     1.4        let
     1.5          val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type
     1.6          val rep_t = Const (Rep_name, abs_T --> rep_T)
     1.7 -        val set_t = Const (set_name, rep_T --> bool_T)
     1.8 +        val set_t = Const (set_name, Type (@{type_name set}, [rep_T]))
     1.9          val set_t' =
    1.10            prop_of_Rep |> HOLogic.dest_Trueprop
    1.11                        |> specialize_type thy (dest_Const rep_t)
    1.12                        |> HOLogic.dest_mem |> snd
    1.13        in
    1.14          [HOLogic.all_const abs_T
    1.15 -         $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
    1.16 +         $ Abs (Name.uu, abs_T, HOLogic.mk_mem (rep_t $ Bound 0, set_t))]
    1.17          |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
    1.18          |> map HOLogic.mk_Trueprop
    1.19        end