fixed Nitpick's typedef handling w.r.t. "set"
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:18 2012 +0100
@@ -1923,14 +1923,14 @@
let
val rep_T = varify_and_instantiate_type ctxt abs_type abs_T rep_type
val rep_t = Const (Rep_name, abs_T --> rep_T)
- val set_t = Const (set_name, rep_T --> bool_T)
+ val set_t = Const (set_name, Type (@{type_name set}, [rep_T]))
val set_t' =
prop_of_Rep |> HOLogic.dest_Trueprop
|> specialize_type thy (dest_Const rep_t)
|> HOLogic.dest_mem |> snd
in
[HOLogic.all_const abs_T
- $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))]
+ $ Abs (Name.uu, abs_T, HOLogic.mk_mem (rep_t $ Bound 0, set_t))]
|> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t'))
|> map HOLogic.mk_Trueprop
end