--- 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,7 +1923,7 @@
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, Type (@{type_name set}, [rep_T]))
+ val set_t = Const (set_name, HOLogic.mk_setT rep_T)
val set_t' =
prop_of_Rep |> HOLogic.dest_Trueprop
|> specialize_type thy (dest_Const rep_t)
@@ -2060,7 +2060,7 @@
| triples =>
let
val binders_T = HOLogic.mk_tupleT (binder_types T)
- val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
+ val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T))
val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
val rel = (("R", j), rel_T)
val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::