# HG changeset patch # User blanchet # Date 1340702079 -7200 # Node ID 1016664b8feb44de2800ae7e4f9e921cef453ae4 # Parent defbcdc60fd65d8da427b0fe4ddc15702078e12b started adding polymophic SPASS output diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200 @@ -118,7 +118,7 @@ let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") - val atp = if format = DFG then spassN else eN + val atp = case format of DFG _ => spassN | _ => eN val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp @@ -174,7 +174,7 @@ let val type_enc = type_enc |> type_enc_from_string Strict |> adjust_type_enc format - val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic + val mono = not (is_type_enc_polymorphic type_enc) val path = file_name |> Path.explode val _ = File.write path "" val facts = facts_of thy @@ -213,7 +213,7 @@ val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) val atp_problem = atp_problem - |> (format <> DFG ? add_inferences_to_problem infers) + |> (case format of DFG _ => I | _ => add_inferences_to_problem infers) |> order_problem_facts name_ord val ord = effective_term_order ctxt eN (* dummy *) val ss = lines_for_atp_problem format ord (K []) atp_problem diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200 @@ -28,7 +28,7 @@ gen_prec : bool, gen_simp : bool} - datatype polymorphism = Monomorphic | Polymorphic + datatype polymorphism = Monomorphic | Polymorphic | Type_Classes datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype thf_defs = THF_Without_Defs | THF_With_Defs @@ -39,7 +39,7 @@ FOF | TFF of polymorphism * tptp_explicitness | THF of polymorphism * tptp_explicitness * thf_choice * thf_defs | - DFG + DFG of polymorphism datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -160,7 +160,7 @@ gen_prec : bool, gen_simp : bool} -datatype polymorphism = Monomorphic | Polymorphic +datatype polymorphism = Monomorphic | Polymorphic | Type_Classes datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype thf_defs = THF_Without_Defs | THF_With_Defs @@ -171,7 +171,7 @@ FOF | TFF of polymorphism * tptp_explicitness | THF of polymorphism * tptp_explicitness * thf_choice * thf_defs | - DFG + DFG of polymorphism datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture datatype 'a problem_line = @@ -306,7 +306,7 @@ | is_format_higher_order _ = false fun is_format_typed (TFF _) = true | is_format_typed (THF _) = true - | is_format_typed DFG = true + | is_format_typed (DFG _) = true | is_format_typed _ = false fun tptp_string_for_role Axiom = "axiom" @@ -336,7 +336,7 @@ fun str_for_type format ty = let - val dfg = (format = DFG) + val dfg = case format of DFG _ => true | _ => false fun str _ (AType (s, [])) = if dfg andalso s = tptp_individual_type then dfg_individual_type else s | str _ (AType (s, tys)) = @@ -438,7 +438,7 @@ | tptp_string_for_format FOF = tptp_fof | tptp_string_for_format (TFF _) = tptp_tff | tptp_string_for_format (THF _) = tptp_thf - | tptp_string_for_format DFG = raise Fail "non-TPTP format" + | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format" fun tptp_string_for_problem_line format (Decl (ident, sym, ty)) = tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ @@ -464,7 +464,7 @@ fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2 | binder_atypes _ = [] -fun dfg_string_for_formula gen_simp info = +fun dfg_string_for_formula poly gen_simp info = let fun suffix_tag top_level s = if top_level then @@ -492,7 +492,7 @@ | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level fun str_for_formula top_level (AQuant (q, xs, phi)) = str_for_quant q ^ "(" ^ "[" ^ - commas (map (string_for_bound_var DFG) xs) ^ "], " ^ + commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^ str_for_formula top_level phi ^ ")" | str_for_formula top_level (AConn (c, phis)) = str_for_conn top_level c ^ "(" ^ @@ -503,19 +503,19 @@ fun maybe_enclose bef aft "" = "% " ^ bef ^ aft | maybe_enclose bef aft s = bef ^ s ^ aft -fun dfg_lines {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = +fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = let fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")" fun ary sym = curry spair sym o arity_of_type fun fun_typ sym ty = - "function(" ^ sym ^ ", " ^ string_for_type DFG ty ^ ")." + "function(" ^ sym ^ ", " ^ string_for_type (DFG poly) ty ^ ")." fun pred_typ sym ty = "predicate(" ^ - commas (sym :: map (string_for_type DFG) (binder_atypes ty)) ^ ")." + commas (sym :: map (string_for_type (DFG poly)) (binder_atypes ty)) ^ ")." fun formula pred (Formula (ident, kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in - "formula(" ^ dfg_string_for_formula gen_simp info phi ^ + "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^ ", " ^ ident ^ (if rank = default_rank then "" else ", " ^ string_of_int rank) ^ ")." |> SOME @@ -587,7 +587,9 @@ fun lines_for_atp_problem format ord ord_info problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: - (if format = DFG then dfg_lines ord ord_info else tptp_lines format) problem + (case format of + DFG poly => dfg_lines poly ord ord_info + | _ => tptp_lines format) problem (** CNF (Metis) and CNF UEQ (Waldmeister) **) @@ -787,7 +789,7 @@ val avoid_clash = case format of TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars - | DFG => avoid_clash_with_dfg_keywords + | DFG _ => avoid_clash_with_dfg_keywords | _ => I val nice_name = nice_name avoid_clash fun nice_type (AType (name, tys)) = diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200 @@ -22,7 +22,6 @@ General | Induction | Intro | Inductive | Elim | Simp | Def type stature = scope * status - datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars datatype type_level = @@ -86,7 +85,7 @@ val atp_irrelevant_consts : string list val atp_schematic_consts_of : term -> typ list Symtab.table val is_type_enc_higher_order : type_enc -> bool - val polymorphism_of_type_enc : type_enc -> polymorphism + val is_type_enc_polymorphic : type_enc -> bool val level_of_type_enc : type_enc -> type_level val is_type_enc_sound : type_enc -> bool val type_enc_from_string : strictness -> string -> type_enc @@ -126,7 +125,12 @@ datatype order = First_Order | Higher_Order of thf_choice -datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic +datatype phantom_policy = Without_Phantom_Type_Vars | With_Phantom_Type_Vars +datatype polymorphism = + Type_Class_Polymorphic | + Raw_Polymorphic of phantom_policy | + Raw_Monomorphic | + Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars datatype type_level = @@ -149,6 +153,12 @@ | polymorphism_of_type_enc (Guards (poly, _)) = poly | polymorphism_of_type_enc (Tags (poly, _)) = poly +fun is_type_enc_polymorphic type_enc = + case polymorphism_of_type_enc type_enc of + Raw_Polymorphic _ => true + | Type_Class_Polymorphic => true + | _ => false + fun level_of_type_enc (Native (_, _, level)) = level | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level @@ -173,10 +183,6 @@ val keep_lamsN = "keep_lams" val lam_liftingN = "lam_lifting" (* legacy *) -(* It's still unclear whether all TFF1 implementations will support type - signatures such as "!>[A : $tType] : $o", with phantom type variables. *) -val avoid_first_order_phantom_type_vars = false - val bound_var_prefix = "B_" val all_bound_var_prefix = "A_" val exist_bound_var_prefix = "E_" @@ -606,15 +612,21 @@ fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE fun type_enc_from_string strictness s = - (case try (unprefix "poly_") s of - SOME s => (SOME Raw_Polymorphic, s) + (case try (unprefix "tc_") s of + SOME s => (SOME Type_Class_Polymorphic, s) | NONE => - case try (unprefix "raw_mono_") s of - SOME s => (SOME Raw_Monomorphic, s) - | NONE => - case try (unprefix "mono_") s of - SOME s => (SOME Mangled_Monomorphic, s) - | NONE => (NONE, s)) + case try (unprefix "poly_") s of + (* It's still unclear whether all TFF1 implementations will support + type signatures such as "!>[A : $tType] : $o", with phantom type + variables. *) + SOME s => (SOME (Raw_Polymorphic With_Phantom_Type_Vars), s) + | NONE => + case try (unprefix "raw_mono_") s of + SOME s => (SOME Raw_Monomorphic, s) + | NONE => + case try (unprefix "mono_") s of + SOME s => (SOME Mangled_Monomorphic, s) + | NONE => (NONE, s)) ||> (fn s => case try_unsuffixes queries s of SOME s => @@ -629,26 +641,25 @@ case (core, (poly, level)) of ("native", (SOME poly, _)) => (case (poly, level) of - (Raw_Polymorphic, All_Types) => - Native (First_Order, Raw_Polymorphic, All_Types) - | (Mangled_Monomorphic, _) => + (Mangled_Monomorphic, _) => if granularity_of_type_level level = All_Vars then Native (First_Order, Mangled_Monomorphic, level) else raise Same.SAME - | _ => raise Same.SAME) + | (Raw_Monomorphic, _) => raise Same.SAME + | (poly, All_Types) => Native (First_Order, poly, All_Types)) | ("native_higher", (SOME poly, _)) => (case (poly, level) of - (Raw_Polymorphic, All_Types) => - Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types) - | (_, Nonmono_Types _) => raise Same.SAME + (_, Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => if granularity_of_type_level level = All_Vars then Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, level) else raise Same.SAME - | _ => raise Same.SAME) + | (Raw_Monomorphic, _) => raise Same.SAME + | (poly, All_Types) => + Native (Higher_Order THF_With_Choice, poly, All_Types)) | ("guards", (SOME poly, _)) => if poly = Mangled_Monomorphic andalso granularity_of_type_level level = Undercover_Vars then @@ -666,7 +677,7 @@ if poly = Mangled_Monomorphic then raise Same.SAME else Guards (poly, Const_Types true) | ("erased", (NONE, All_Types (* naja *))) => - Guards (Raw_Polymorphic, No_Types) + Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) | _ => raise Same.SAME) handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") @@ -682,7 +693,9 @@ Native (adjust_order choice order, Mangled_Monomorphic, level) | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) - | adjust_type_enc DFG (Native (_, _, level)) = + | adjust_type_enc (DFG Polymorphic) (Native (_, poly, level)) = + Native (First_Order, poly, level) + | adjust_type_enc (DFG Monomorphic) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc (TFF _) (Native (_, poly, level)) = Native (First_Order, poly, level) @@ -774,7 +787,7 @@ fun lift_lams_part_1 ctxt type_enc = map close_form #> rpair ctxt #-> Lambda_Lifting.lift_lambdas - (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then + (SOME ((if is_type_enc_polymorphic type_enc then lam_lifted_poly_prefix else lam_lifted_mono_prefix) ^ "_a")) @@ -839,7 +852,8 @@ if s = type_tag_name then if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args else case type_enc of - Native (_, Raw_Polymorphic, _) => All_Type_Args + Native (_, Raw_Polymorphic _, _) => All_Type_Args + | Native (_, Type_Class_Polymorphic, _) => All_Type_Args | Tags (_, All_Types) => No_Type_Args | _ => let val level = level_of_type_enc type_enc in @@ -877,9 +891,8 @@ fun type_class_formula type_enc class arg = AAtom (ATerm (class, arg :: (case type_enc of - Native (First_Order, Raw_Polymorphic, _) => - if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])] - else [] + Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) => + [ATerm (TYPE_name, [arg])] | _ => []))) fun formulas_for_types type_enc add_sorts_on_typ Ts = [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts @@ -981,7 +994,7 @@ fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) | to_poly_atype _ = raise Fail "unexpected type abstraction" val to_atype = - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype + if is_type_enc_polymorphic type_enc then to_poly_atype else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty @@ -1703,7 +1716,9 @@ @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))] |> map (apsnd (map (apsnd zero_var_indexes))) -fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types +fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types + | atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) = + SOME atype_of_types (* ### FIXME *) | atype_of_type_vars _ = NONE fun bound_tvars type_enc sorts Ts = @@ -1730,7 +1745,7 @@ val type_tag = `(make_fixed_const NONE) type_tag_name fun could_specialize_helpers type_enc = - polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso + not (is_type_enc_polymorphic type_enc) andalso level_of_type_enc type_enc <> No_Types fun should_specialize_helper type_enc t = could_specialize_helpers type_enc andalso @@ -2118,7 +2133,7 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) -fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true +fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true | type_enc_needs_free_types (Native _) = false | type_enc_needs_free_types _ = true @@ -2136,12 +2151,12 @@ (** Symbol declarations **) -fun decl_line_for_class order s = +fun decl_line_for_class order phantoms s = let val name as (s, _) = `make_type_class s in Decl (sym_decl_prefix ^ s, name, if order = First_Order then ATyAbs ([tvar_a_name], - if avoid_first_order_phantom_type_vars then + if phantoms = Without_Phantom_Type_Vars then AFun (a_itself_atype, bool_atype) else bool_atype) @@ -2151,8 +2166,8 @@ fun decl_lines_for_classes type_enc classes = case type_enc of - Native (order, Raw_Polymorphic, _) => - map (decl_line_for_class order) classes + Native (order, Raw_Polymorphic phantoms, _) => + map (decl_line_for_class order phantoms) classes | _ => [] fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) = @@ -2192,7 +2207,7 @@ fold add_formula_var_types phis | add_formula_var_types _ = I fun var_types () = - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a] + if is_type_enc_polymorphic type_enc then [tvar_a] else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let @@ -2217,9 +2232,8 @@ ? (fold (fold add_fact_syms) [conjs, facts] #> fold add_iterm_syms extra_tms #> (case type_enc of - Native (First_Order, Raw_Polymorphic, _) => - if avoid_first_order_phantom_type_vars then add_TYPE_const () - else I + Native (First_Order, Raw_Polymorphic phantoms, _) => + phantoms = Without_Phantom_Type_Vars ? add_TYPE_const () | Native _ => I | _ => fold add_undefined_const (var_types ()))) end @@ -2284,7 +2298,7 @@ add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift fun monotonic_types_for_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in - [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso + [] |> (is_type_enc_polymorphic type_enc andalso is_type_level_monotonicity_based level andalso granularity_of_type_level level <> Undercover_Vars) ? fold (add_fact_monotonic_types ctxt mono type_enc) facts @@ -2631,7 +2645,7 @@ Full_App_Op_And_Predicator else if length facts + length hyp_ts > app_op_and_predicator_threshold then - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op + if is_type_enc_polymorphic type_enc then Min_App_Op else Sufficient_App_Op else Sufficient_App_Op_And_Predicator @@ -2680,6 +2694,8 @@ map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter) (not exporter) mono type_enc (rank_of_fact_num num_facts)) (0 upto num_facts - 1 ~~ facts) + val class_rel_lines = + map (formula_line_for_class_rel_clause type_enc) class_rel_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers |> map (formula_line_for_fact ctxt helper_prefix I false true mono @@ -2689,8 +2705,7 @@ [(explicit_declsN, class_decl_lines @ sym_decl_lines), (uncurried_alias_eqsN, uncurried_alias_eq_lines), (factsN, fact_lines), - (class_relsN, - map (formula_line_for_class_rel_clause type_enc) class_rel_clauses), + (class_relsN, class_rel_lines), (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses), (helpersN, helper_lines), (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)), diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200 @@ -54,6 +54,7 @@ val satallaxN : string val snarkN : string val spassN : string + val spass_polyN : string val vampireN : string val waldmeisterN : string val z3_tptpN : string @@ -149,6 +150,7 @@ val satallaxN = "satallax" val snarkN = "snark" val spassN = "spass" +val spass_polyN = "spass_poly" val vampireN = "vampire" val waldmeisterN = "waldmeister" val z3_tptpN = "z3_tptp" @@ -409,14 +411,14 @@ prem_role = Conjecture, best_slices = fn _ => (* FUDGE *) - [(0.1667, (false, ((150, DFG, "mono_native", combsN, true), ""))), - (0.1667, (false, ((500, DFG, "mono_native", liftingN, true), spass_H2SOS))), - (0.1666, (false, ((50, DFG, "mono_native", liftingN, true), spass_H2LR0LT0))), - (0.1000, (false, ((250, DFG, "mono_native", combsN, true), spass_H2NuVS0))), - (0.1000, (false, ((1000, DFG, "mono_native", liftingN, true), spass_H1SOS))), - (0.1000, (false, ((150, DFG, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))), - (0.1000, (false, ((300, DFG, "mono_native", combsN, true), spass_H2SOS))), - (0.1000, (false, ((100, DFG, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))], + [(0.1667, (false, ((150, DFG Monomorphic, "mono_native", combsN, true), ""))), + (0.1667, (false, ((500, DFG Monomorphic, "mono_native", liftingN, true), spass_H2SOS))), + (0.1666, (false, ((50, DFG Monomorphic, "mono_native", liftingN, true), spass_H2LR0LT0))), + (0.1000, (false, ((250, DFG Monomorphic, "mono_native", combsN, true), spass_H2NuVS0))), + (0.1000, (false, ((1000, DFG Monomorphic, "mono_native", liftingN, true), spass_H1SOS))), + (0.1000, (false, ((150, DFG Monomorphic, "poly_guards??", liftingN, false), spass_H2NuVS0Red2))), + (0.1000, (false, ((300, DFG Monomorphic, "mono_native", combsN, true), spass_H2SOS))), + (0.1000, (false, ((100, DFG Monomorphic, "mono_native", combs_and_liftingN, true), spass_H2NuVS0)))], best_max_mono_iters = default_max_mono_iters, best_max_new_mono_instances = default_max_new_mono_instances} @@ -495,7 +497,7 @@ val z3_tptp = (z3_tptpN, fn () => z3_tptp_config) -(* Not really a prover: Experimental Polymorphic TFF and THF output *) +(* Not really a prover: Experimental Polymorphic THF and DFG output *) fun dummy_config format type_enc : atp_config = {exec = (["ISABELLE_ATP"], "scripts/dummy_atp"), @@ -516,6 +518,9 @@ val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) +val spass_poly_format = DFG Polymorphic +val spass_poly_config = dummy_config spass_poly_format "tc_native" +val spass_poly = (spass_polyN, fn () => spass_poly_config) (* Remote ATP invocation via SystemOnTPTP *) @@ -667,8 +672,8 @@ end val atps= - [alt_ergo, e, leo2, dummy_thf, satallax, spass, vampire, z3_tptp, remote_e, - remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, + [alt_ergo, e, leo2, satallax, spass, spass_poly, vampire, z3_tptp, dummy_thf, + remote_e, remote_e_sine, remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_z3_tptp, remote_snark, remote_waldmeister] diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200 @@ -211,7 +211,7 @@ fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = let val (conj_clauses, fact_clauses) = - if polymorphism_of_type_enc type_enc = Raw_Polymorphic then + if is_type_enc_polymorphic type_enc then (conj_clauses, fact_clauses) else conj_clauses @ fact_clauses diff -r defbcdc60fd6 -r 1016664b8feb src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200 @@ -717,7 +717,7 @@ |> not sound ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |> take num_facts - |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic + |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd prop_of) |> prepare_atp_problem ctxt format prem_role type_enc