src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46091 472c952d42dd
parent 46089 d98eb715444d
child 46094 4d9a5f1514b4
     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 @@ -1821,13 +1821,17 @@
     1.4        val dom_T = pseudo_domain_type T
     1.5        val ran_T = pseudo_range_type T
     1.6        val var_t = Var (("x", j), dom_T)
     1.7 -    in
     1.8 -      extensional_equal (j + 1) ran_T (betapply (t1, var_t))
     1.9 -                        (betapply (t2, var_t))
    1.10 -    end
    1.11 +      fun apply fun_t arg_t =
    1.12 +        if is_fun_type T then
    1.13 +          betapply (fun_t, arg_t)
    1.14 +        else
    1.15 +          Const (@{const_name Set.member}, dom_T --> T --> ran_T)
    1.16 +          $ arg_t $ fun_t
    1.17 +    in extensional_equal (j + 1) ran_T (apply t1 var_t) (apply t2 var_t) end
    1.18    else
    1.19      Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
    1.20  
    1.21 +(* FIXME: needed? *)
    1.22  fun equationalize_term ctxt tag t =
    1.23    let
    1.24      val j = maxidx_of_term t + 1