# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 299d4266a9f9d35a0ac47a1584f9eef20e03a398
# Parent  93f58e6a6f3ea58495d4760aa8f1bce3fe92e752
avoid Type.TYPE_MATCH exception for "True_or_False" for "If"

diff -r 93f58e6a6f3e -r 299d4266a9f9 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -388,12 +388,14 @@
       fun dub_and_inst c needs_full_types (th, j) =
         ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
           false),
-         th |> prop_of
-            |> general_type_arg_policy type_sys = Mangled_Types
-               ? (case typ of
-                    SOME T =>
-                    specialize_type thy (safe_invert_const unmangled_s, T)
-                  | NONE => I))
+         let val t = th |> prop_of in
+           t |> (general_type_arg_policy type_sys = Mangled_Types andalso
+                 not (null (Term.hidden_polymorphism t)))
+                ? (case typ of
+                     SOME T =>
+                     specialize_type thy (safe_invert_const unmangled_s, T)
+                   | NONE => I)
+         end)
       fun make_facts eq_as_iff =
         map_filter (make_fact ctxt false eq_as_iff false)
     in