# HG changeset patch
# User blanchet
# Date 1337698767 -7200
# Node ID 2a420750248bc107aecd277c6c7c420803702009
# Parent  a2a821abab83d7d26f1010e271169b6773c50244
don't apply "ext_cong_neq" to biimplications

diff -r a2a821abab83 -r 2a420750248b src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Tue May 22 16:59:27 2012 +0200
@@ -574,7 +574,7 @@
 
 exception NO_F_PATTERN of unit
 
-fun get_F_pattern t u =
+fun get_F_pattern T t u =
   let
     fun pat t u =
       let
@@ -593,11 +593,13 @@
           end
       end
   in
-    (case pat t u of
-       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
-     | _ => NONE)
-    handle NO_F_PATTERN () => NONE
+    if T = @{typ bool} then
+      NONE
+    else case pat t u of
+      (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
+    | _ => NONE
   end
+  handle NO_F_PATTERN () => NONE
 
 val ext_cong_neq = @{thm ext_cong_neq}
 val F_ext_cong_neq =
@@ -608,9 +610,10 @@
 (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
 fun cong_extensionalize_thm thy th =
   case concl_of th of
-    @{const Trueprop} $ (@{const Not} $ (Const (@{const_name HOL.eq}, _)
-                                         $ (t as _ $ _) $ (u as _ $ _))) =>
-    (case get_F_pattern t u of
+    @{const Trueprop} $ (@{const Not}
+        $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
+           $ (t as _ $ _) $ (u as _ $ _))) =>
+    (case get_F_pattern T t u of
        SOME p =>
        let val inst = [pairself (cterm_of thy) (F_ext_cong_neq, p)] in
          th RS cterm_instantiate inst ext_cong_neq