# 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