src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46089 d98eb715444d
parent 46088 948bef826443
child 46091 472c952d42dd
     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,7 +1923,7 @@
     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, Type (@{type_name set}, [rep_T]))
     1.8 +        val set_t = Const (set_name, HOLogic.mk_setT 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 @@ -2060,7 +2060,7 @@
    1.13       | triples =>
    1.14         let
    1.15           val binders_T = HOLogic.mk_tupleT (binder_types T)
    1.16 -         val rel_T = HOLogic.mk_prodT (binders_T, binders_T) --> bool_T
    1.17 +         val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T))
    1.18           val j = fold Integer.max (map maxidx_of_term intro_ts) 0 + 1
    1.19           val rel = (("R", j), rel_T)
    1.20           val prop = Const (@{const_name wf}, rel_T --> bool_T) $ Var rel ::