src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46244 549755ebf4d2
parent 46219 426ed18eba43
child 46320 0b8b73b49848
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 17 18:25:36 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 17 18:25:36 2012 +0100
     1.3 @@ -1823,18 +1823,15 @@
     1.4  (** Axiom extraction/generation **)
     1.5  
     1.6  fun extensional_equal j T t1 t2 =
     1.7 -  if is_fun_or_set_type T then
     1.8 +  if is_fun_type T then
     1.9      let
    1.10        val dom_T = pseudo_domain_type T
    1.11        val ran_T = pseudo_range_type T
    1.12        val var_t = Var (("x", j), dom_T)
    1.13 -      fun apply fun_t arg_t =
    1.14 -        if is_fun_type T then
    1.15 -          betapply (fun_t, arg_t)
    1.16 -        else
    1.17 -          Const (@{const_name Set.member}, dom_T --> T --> ran_T)
    1.18 -          $ arg_t $ fun_t
    1.19 -    in extensional_equal (j + 1) ran_T (apply t1 var_t) (apply t2 var_t) end
    1.20 +    in
    1.21 +      extensional_equal (j + 1) ran_T (betapply (t1, var_t))
    1.22 +                        (betapply (t2, var_t))
    1.23 +    end
    1.24    else
    1.25      Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
    1.26