# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 472c952d42ddb0b57ae6f375aaf4417bbb5a265a
# Parent  f1796596ef6078b355627300f5dc293acf85c818
fixed set extensionality code

diff -r f1796596ef60 -r 472c952d42dd src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
@@ -1821,13 +1821,17 @@
       val dom_T = pseudo_domain_type T
       val ran_T = pseudo_range_type T
       val var_t = Var (("x", j), dom_T)
-    in
-      extensional_equal (j + 1) ran_T (betapply (t1, var_t))
-                        (betapply (t2, var_t))
-    end
+      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
   else
     Const (@{const_name HOL.eq}, T --> T --> bool_T) $ t1 $ t2
 
+(* FIXME: needed? *)
 fun equationalize_term ctxt tag t =
   let
     val j = maxidx_of_term t + 1