--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 17 18:25:36 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 17 18:25:36 2012 +0100
@@ -1823,18 +1823,15 @@
(** Axiom extraction/generation **)
fun extensional_equal j T t1 t2 =
- if is_fun_or_set_type T then
+ if is_fun_type T then
let
val dom_T = pseudo_domain_type T
val ran_T = pseudo_range_type T
val var_t = Var (("x", j), dom_T)
- fun apply fun_t arg_t =
- if is_fun_type T then
- betapply (fun_t, arg_t)
- else
- Const (@{const_name Set.member}, dom_T --> T --> ran_T)
- $ arg_t $ fun_t
- in extensional_equal (j + 1) ran_T (apply t1 var_t) (apply t2 var_t) end
+ in
+ extensional_equal (j + 1) ran_T (betapply (t1, var_t))
+ (betapply (t2, var_t))
+ end
else
Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2