# HG changeset patch
# User blanchet
# Date 1326821136 -3600
# Node ID 549755ebf4d26393c732ae1d316f0b3f625992bc
# Parent  4b1b43ab7c62ef0a9b49cb854411694991200dab
fixed a bug introduced when porting functions to set -- extensionality on sets break the form of equations expected elsewhere by Nitpick

diff -r 4b1b43ab7c62 -r 549755ebf4d2 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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