src/HOL/Tools/Meson/meson.ML

     skolemize_with_choice_theorems ctxt (choice_theorems thy)
   end
 
 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
         val ((head1, args1), (head2, args2)) = (t, u) |> pairself strip_comb
       in

           let val T = fastype_of t in
             if can dest_funT T then (SOME T, Bound 0) else raise NO_F_PATTERN ()
           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 =
   Term.add_vars (prop_of @{thm ext_cong_neq}) []
   |> filter (fn ((s, _), _) => s = "F")
   |> the_single |> Var
 
 (* 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
        end
      | NONE => th)