1.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -89,12 +89,19 @@
     1.4    end
     1.5    |> Meson.make_meta_clause
     1.6  
     1.7 -val clause_params =
     1.8 +fun clause_params type_enc =
     1.9    {ordering = Metis_KnuthBendixOrder.default,
    1.10 -   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    1.11 +   orderLiterals =
    1.12 +     (* Type axioms seem to benefit from the positive literal order, but for
    1.13 +        compatibility we keep the unsigned order for Metis's default
    1.14 +        "partial_types" mode. *)
    1.15 +     if is_type_enc_fairly_sound type_enc then
    1.16 +       Metis_Clause.PositiveLiteralOrder
    1.17 +     else
    1.18 +       Metis_Clause.UnsignedLiteralOrder,
    1.19     orderTerms = true}
    1.20 -val active_params =
    1.21 -  {clause = clause_params,
    1.22 +fun active_params type_enc =
    1.23 +  {clause = clause_params type_enc,
    1.24     prefactor = #prefactor Metis_Active.default,
    1.25     postfactor = #postfactor Metis_Active.default}
    1.26  val waiting_params =
    1.27 @@ -102,7 +109,8 @@
    1.28     variablesWeight = 0.0,
    1.29     literalsWeight = 0.0,
    1.30     models = []}
    1.31 -val resolution_params = {active = active_params, waiting = waiting_params}
    1.32 +fun resolution_params type_enc =
    1.33 +  {active = active_params type_enc, waiting = waiting_params}
    1.34  
    1.35  (* Main function to start Metis proof and reconstruction *)
    1.36  fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
    1.37 @@ -120,6 +128,8 @@
    1.38        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    1.39        val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    1.40        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    1.41 +      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    1.42 +      val type_enc = type_enc_from_string Unsound type_enc
    1.43        val (sym_tab, axioms, old_skolems) =
    1.44          prepare_metis_problem ctxt type_enc cls ths
    1.45        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    1.46 @@ -129,13 +139,13 @@
    1.47        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    1.48        val thms = axioms |> map fst
    1.49        val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    1.50 -      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
    1.51        val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    1.52    in
    1.53        case filter (fn t => prop_of t aconv @{prop False}) cls of
    1.54            false_th :: _ => [false_th RS @{thm FalseE}]
    1.55          | [] =>
    1.56 -      case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    1.57 +      case Metis_Resolution.new (resolution_params type_enc)
    1.58 +                                {axioms = thms, conjecture = []}
    1.59             |> Metis_Resolution.loop of
    1.60            Metis_Resolution.Contradiction mth =>
    1.61              let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^

     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -9,6 +9,8 @@
     2.4  
     2.5  signature METIS_TRANSLATE =
     2.6  sig
     2.7 +  type type_enc = ATP_Translate.type_enc
     2.8 +
     2.9    datatype isa_thm =
    2.10      Isa_Reflexive_or_Trivial |
    2.11      Isa_Raw of thm
    2.12 @@ -25,7 +27,7 @@
    2.13    val metis_name_table : ((string * int) * (string * bool)) list
    2.14    val reveal_old_skolem_terms : (string * term) list -> term -> term
    2.15    val prepare_metis_problem :
    2.16 -    Proof.context -> string -> thm list -> thm list
    2.17 +    Proof.context -> type_enc -> thm list -> thm list
    2.18      -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
    2.19  end
    2.20  
    2.21 @@ -167,7 +169,6 @@
    2.22  (* Function to generate metis clauses, including comb and type clauses *)
    2.23  fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
    2.24    let
    2.25 -    val type_enc = type_enc_from_string Unsound type_enc
    2.26      val (conj_clauses, fact_clauses) =
    2.27        if polymorphism_of_type_enc type_enc = Polymorphic then
    2.28          (conj_clauses, fact_clauses)