1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 25 14:25:06 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Aug 25 14:25:07 2011 +0200
     1.3 @@ -9,14 +9,16 @@
     1.4  
     1.5  signature METIS_RECONSTRUCT =
     1.6  sig
     1.7 +  type type_enc = ATP_Translate.type_enc
     1.8 +
     1.9    exception METIS of string * string
    1.10  
    1.11    val hol_clause_from_metis :
    1.12 -    Proof.context -> int Symtab.table -> (string * term) list -> Metis_Thm.thm
    1.13 -    -> term
    1.14 +    Proof.context -> type_enc -> int Symtab.table -> (string * term) list
    1.15 +    -> Metis_Thm.thm -> term
    1.16    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    1.17    val replay_one_inference :
    1.18 -    Proof.context -> (string * term) list -> int Symtab.table
    1.19 +    Proof.context -> type_enc -> (string * term) list -> int Symtab.table
    1.20      -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
    1.21      -> (Metis_Thm.thm * thm) list
    1.22    val discharge_skolem_premises :
    1.23 @@ -33,38 +35,39 @@
    1.24  
    1.25  exception METIS of string * string
    1.26  
    1.27 -fun atp_name_from_metis s =
    1.28 -  case find_first (fn (_, (s', _)) => s' = s) metis_name_table of
    1.29 +fun atp_name_from_metis type_enc s =
    1.30 +  case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
    1.31      SOME ((s, _), (_, swap)) => (s, swap)
    1.32    | _ => (s, false)
    1.33 -fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
    1.34 -    let val (s, swap) = atp_name_from_metis (Metis_Name.toString s) in
    1.35 -      ATerm (s, tms |> map atp_term_from_metis |> swap ? rev)
    1.36 +fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
    1.37 +    let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
    1.38 +      ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
    1.39      end
    1.40 -  | atp_term_from_metis (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
    1.41 +  | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
    1.42  
    1.43 -fun hol_term_from_metis ctxt sym_tab =
    1.44 -  atp_term_from_metis #> term_from_atp ctxt false sym_tab NONE
    1.45 +fun hol_term_from_metis ctxt type_enc sym_tab =
    1.46 +  atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
    1.47  
    1.48 -fun atp_literal_from_metis (pos, atom) =
    1.49 -  atom |> Metis_Term.Fn |> atp_term_from_metis |> AAtom |> not pos ? mk_anot
    1.50 -fun atp_clause_from_metis [] = AAtom (ATerm (tptp_false, []))
    1.51 -  | atp_clause_from_metis lits =
    1.52 -    lits |> map atp_literal_from_metis |> mk_aconns AOr
    1.53 +fun atp_literal_from_metis type_enc (pos, atom) =
    1.54 +  atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
    1.55 +       |> AAtom |> not pos ? mk_anot
    1.56 +fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
    1.57 +  | atp_clause_from_metis type_enc lits =
    1.58 +    lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
    1.59  
    1.60  fun reveal_old_skolems_and_infer_types ctxt old_skolems =
    1.61    map (reveal_old_skolem_terms old_skolems)
    1.62    #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
    1.63  
    1.64 -fun hol_clause_from_metis ctxt sym_tab old_skolems =
    1.65 +fun hol_clause_from_metis ctxt type_enc sym_tab old_skolems =
    1.66    Metis_Thm.clause
    1.67    #> Metis_LiteralSet.toList
    1.68 -  #> atp_clause_from_metis
    1.69 +  #> atp_clause_from_metis type_enc
    1.70    #> prop_from_atp ctxt false sym_tab
    1.71    #> singleton (reveal_old_skolems_and_infer_types ctxt old_skolems)
    1.72  
    1.73 -fun hol_terms_from_metis ctxt old_skolems sym_tab fol_tms =
    1.74 -  let val ts = map (hol_term_from_metis ctxt sym_tab) fol_tms
    1.75 +fun hol_terms_from_metis ctxt type_enc old_skolems sym_tab fol_tms =
    1.76 +  let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
    1.77        val _ = trace_msg ctxt (fn () => "  calling type inference:")
    1.78        val _ = app (fn t => trace_msg ctxt
    1.79                                       (fn () => Syntax.string_of_term ctxt t)) ts
    1.80 @@ -111,10 +114,10 @@
    1.81        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
    1.82    in  cterm_instantiate substs th  end;
    1.83  
    1.84 -fun assume_inference ctxt old_skolems sym_tab atom =
    1.85 +fun assume_inference ctxt type_enc old_skolems sym_tab atom =
    1.86    inst_excluded_middle
    1.87        (Proof_Context.theory_of ctxt)
    1.88 -      (singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
    1.89 +      (singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
    1.90                   (Metis_Term.Fn atom))
    1.91  
    1.92  (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
    1.93 @@ -122,7 +125,7 @@
    1.94     sorts. Instead we try to arrange that new TVars are distinct and that types
    1.95     can be inferred from terms. *)
    1.96  
    1.97 -fun inst_inference ctxt old_skolems sym_tab th_pairs fsubst th =
    1.98 +fun inst_inference ctxt type_enc old_skolems sym_tab th_pairs fsubst th =
    1.99    let val thy = Proof_Context.theory_of ctxt
   1.100        val i_th = lookth th_pairs th
   1.101        val i_th_vars = Term.add_vars (prop_of i_th) []
   1.102 @@ -130,7 +133,7 @@
   1.103        fun subst_translation (x,y) =
   1.104          let val v = find_var x
   1.105              (* We call "reveal_old_skolems_and_infer_types" below. *)
   1.106 -            val t = hol_term_from_metis ctxt sym_tab y
   1.107 +            val t = hol_term_from_metis ctxt type_enc sym_tab y
   1.108          in  SOME (cterm_of thy (Var v), t)  end
   1.109          handle Option.Option =>
   1.110                 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   1.111 @@ -255,7 +258,7 @@
   1.112  (* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
   1.113  val select_literal = negate_head oo make_last
   1.114  
   1.115 -fun resolve_inference ctxt old_skolems sym_tab th_pairs atom th1 th2 =
   1.116 +fun resolve_inference ctxt type_enc old_skolems sym_tab th_pairs atom th1 th2 =
   1.117    let
   1.118      val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
   1.119      val _ = trace_msg ctxt (fn () =>
   1.120 @@ -271,7 +274,7 @@
   1.121        let
   1.122          val thy = Proof_Context.theory_of ctxt
   1.123          val i_atom =
   1.124 -          singleton (hol_terms_from_metis ctxt old_skolems sym_tab)
   1.125 +          singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab)
   1.126                      (Metis_Term.Fn atom)
   1.127          val _ = trace_msg ctxt (fn () =>
   1.128                      "  atom: " ^ Syntax.string_of_term ctxt i_atom)
   1.129 @@ -300,10 +303,11 @@
   1.130  val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
   1.131  val refl_idx = 1 + Thm.maxidx_of REFL_THM;
   1.132  
   1.133 -fun refl_inference ctxt old_skolems sym_tab t =
   1.134 +fun refl_inference ctxt type_enc old_skolems sym_tab t =
   1.135    let
   1.136      val thy = Proof_Context.theory_of ctxt
   1.137 -    val i_t = singleton (hol_terms_from_metis ctxt old_skolems sym_tab) t
   1.138 +    val i_t =
   1.139 +      singleton (hol_terms_from_metis ctxt type_enc old_skolems sym_tab) t
   1.140      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.141      val c_t = cterm_incr_types thy refl_idx i_t
   1.142    in cterm_instantiate [(refl_x, c_t)] REFL_THM end
   1.143 @@ -313,11 +317,11 @@
   1.144  val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
   1.145  val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
   1.146  
   1.147 -fun equality_inference ctxt old_skolems sym_tab (pos, atom) fp fr =
   1.148 +fun equality_inference ctxt type_enc old_skolems sym_tab (pos, atom) fp fr =
   1.149    let val thy = Proof_Context.theory_of ctxt
   1.150        val m_tm = Metis_Term.Fn atom
   1.151        val [i_atom, i_tm] =
   1.152 -        hol_terms_from_metis ctxt old_skolems sym_tab [m_tm, fr]
   1.153 +        hol_terms_from_metis ctxt type_enc old_skolems sym_tab [m_tm, fr]
   1.154        val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.155        fun replace_item_list lx 0 (_::ls) = lx::ls
   1.156          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.157 @@ -336,7 +340,8 @@
   1.158                                         #> the #> unmangled_const_name))
   1.159            in
   1.160              if s = metis_predicator orelse s = predicator_name orelse
   1.161 -               s = metis_type_tag orelse s = type_tag_name then
   1.162 +               s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
   1.163 +               orelse s = type_tag_name then
   1.164                path_finder tm ps (nth ts p)
   1.165              else if s = metis_app_op orelse s = app_op_name then
   1.166                let
   1.167 @@ -377,21 +382,22 @@
   1.168  
   1.169  val factor = Seq.hd o distinct_subgoals_tac
   1.170  
   1.171 -fun one_step ctxt old_skolems sym_tab th_pairs p =
   1.172 +fun one_step ctxt type_enc old_skolems sym_tab th_pairs p =
   1.173    case p of
   1.174      (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
   1.175    | (_, Metis_Proof.Assume f_atom) =>
   1.176 -    assume_inference ctxt old_skolems sym_tab f_atom
   1.177 +    assume_inference ctxt type_enc old_skolems sym_tab f_atom
   1.178    | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
   1.179 -    inst_inference ctxt old_skolems sym_tab th_pairs f_subst f_th1
   1.180 +    inst_inference ctxt type_enc old_skolems sym_tab th_pairs f_subst f_th1
   1.181      |> factor
   1.182    | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
   1.183 -    resolve_inference ctxt old_skolems sym_tab th_pairs f_atom f_th1 f_th2
   1.184 +    resolve_inference ctxt type_enc old_skolems sym_tab th_pairs f_atom f_th1
   1.185 +                      f_th2
   1.186      |> factor
   1.187    | (_, Metis_Proof.Refl f_tm) =>
   1.188 -    refl_inference ctxt old_skolems sym_tab f_tm
   1.189 +    refl_inference ctxt type_enc old_skolems sym_tab f_tm
   1.190    | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
   1.191 -    equality_inference ctxt old_skolems sym_tab f_lit f_p f_r
   1.192 +    equality_inference ctxt type_enc old_skolems sym_tab f_lit f_p f_r
   1.193  
   1.194  fun flexflex_first_order th =
   1.195    case Thm.tpairs_of th of
   1.196 @@ -443,7 +449,8 @@
   1.197        end
   1.198    end
   1.199  
   1.200 -fun replay_one_inference ctxt old_skolems sym_tab (fol_th, inf) th_pairs =
   1.201 +fun replay_one_inference ctxt type_enc old_skolems sym_tab (fol_th, inf)
   1.202 +                         th_pairs =
   1.203    if not (null th_pairs) andalso
   1.204       prop_of (snd (hd th_pairs)) aconv @{prop False} then
   1.205      (* Isabelle sometimes identifies literals (premises) that are distinct in
   1.206 @@ -458,7 +465,7 @@
   1.207                    (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   1.208        val _ = trace_msg ctxt
   1.209                    (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   1.210 -      val th = one_step ctxt old_skolems sym_tab th_pairs (fol_th, inf)
   1.211 +      val th = one_step ctxt type_enc old_skolems sym_tab th_pairs (fol_th, inf)
   1.212                 |> flexflex_first_order
   1.213                 |> resynchronize ctxt fol_th
   1.214        val _ = trace_msg ctxt

     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:25:06 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Thu Aug 25 14:25:07 2011 +0200
     2.3 @@ -74,9 +74,9 @@
     2.4     "t => t'", where "t" and "t'" are the same term modulo type tags.
     2.5     In Isabelle, type tags are stripped away, so we are left with "t = t" or
     2.6     "t => t". Type tag idempotence is also handled this way. *)
     2.7 -fun reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth =
     2.8 +fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth =
     2.9    let val thy = Proof_Context.theory_of ctxt in
    2.10 -    case hol_clause_from_metis ctxt sym_tab old_skolems mth of
    2.11 +    case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of
    2.12        Const (@{const_name HOL.eq}, _) $ _ $ t =>
    2.13        let
    2.14          val ct = cterm_of thy t
    2.15 @@ -91,14 +91,7 @@
    2.16  
    2.17  fun clause_params type_enc =
    2.18    {ordering = Metis_KnuthBendixOrder.default,
    2.19 -   orderLiterals =
    2.20 -     (* Type axioms seem to benefit from the positive literal order, but for
    2.21 -        compatibility we keep the unsigned order for Metis's default
    2.22 -        "partial_types" mode. *)
    2.23 -     if is_type_enc_fairly_sound type_enc then
    2.24 -       Metis_Clause.PositiveLiteralOrder
    2.25 -     else
    2.26 -       Metis_Clause.UnsignedLiteralOrder,
    2.27 +   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    2.28     orderTerms = true}
    2.29  fun active_params type_enc =
    2.30    {clause = clause_params type_enc,
    2.31 @@ -133,7 +126,7 @@
    2.32        val (sym_tab, axioms, old_skolems) =
    2.33          prepare_metis_problem ctxt type_enc cls ths
    2.34        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    2.35 -          reflexive_or_trivial_from_metis ctxt sym_tab old_skolems mth
    2.36 +          reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth
    2.37          | get_isa_thm _ (Isa_Raw ith) = ith
    2.38        val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    2.39        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    2.40 @@ -155,7 +148,7 @@
    2.41                  val proof = Metis_Proof.proof mth
    2.42                  val result =
    2.43                    axioms
    2.44 -                  |> fold (replay_one_inference ctxt' old_skolems sym_tab) proof
    2.45 +                  |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof
    2.46                  val used = map_filter (used_axioms axioms) proof
    2.47                  val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    2.48                  val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Thu Aug 25 14:25:06 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Thu Aug 25 14:25:07 2011 +0200
     3.3 @@ -18,13 +18,14 @@
     3.4    val metis_equal : string
     3.5    val metis_predicator : string
     3.6    val metis_app_op : string
     3.7 -  val metis_type_tag : string
     3.8 +  val metis_systematic_type_tag : string
     3.9 +  val metis_ad_hoc_type_tag : string
    3.10    val metis_generated_var_prefix : string
    3.11    val trace : bool Config.T
    3.12    val verbose : bool Config.T
    3.13    val trace_msg : Proof.context -> (unit -> string) -> unit
    3.14    val verbose_warning : Proof.context -> string -> unit
    3.15 -  val metis_name_table : ((string * int) * (string * bool)) list
    3.16 +  val metis_name_table : ((string * int) * ((type_enc -> string) * bool)) list
    3.17    val reveal_old_skolem_terms : (string * term) list -> term -> term
    3.18    val prepare_metis_problem :
    3.19      Proof.context -> type_enc -> thm list -> thm list
    3.20 @@ -39,8 +40,10 @@
    3.21  
    3.22  val metis_equal = "="
    3.23  val metis_predicator = "{}"
    3.24 -val metis_app_op = "."
    3.25 -val metis_type_tag = ":"
    3.26 +val metis_app_op = Metis_Name.toString Metis_Term.appName
    3.27 +val metis_systematic_type_tag =
    3.28 +  Metis_Name.toString Metis_Term.hasTypeFunctionName
    3.29 +val metis_ad_hoc_type_tag = "**"
    3.30  val metis_generated_var_prefix = "_"
    3.31  
    3.32  val trace = Attrib.setup_config_bool @{binding metis_trace} (K false)
    3.33 @@ -51,11 +54,13 @@
    3.34    if Config.get ctxt verbose then warning ("Metis: " ^ msg) else ()
    3.35  
    3.36  val metis_name_table =
    3.37 -  [((tptp_equal, 2), (metis_equal, false)),
    3.38 -   ((tptp_old_equal, 2), (metis_equal, false)),
    3.39 -   ((prefixed_predicator_name, 1), (metis_predicator, false)),
    3.40 -   ((prefixed_app_op_name, 2), (metis_app_op, false)),
    3.41 -   ((prefixed_type_tag_name, 2), (metis_type_tag, true))]
    3.42 +  [((tptp_equal, 2), (K metis_equal, false)),
    3.43 +   ((tptp_old_equal, 2), (K metis_equal, false)),
    3.44 +   ((prefixed_predicator_name, 1), (K metis_predicator, false)),
    3.45 +   ((prefixed_app_op_name, 2), (K metis_app_op, false)),
    3.46 +   ((prefixed_type_tag_name, 2),
    3.47 +    (fn Tags (_, All_Types, Uniform) => metis_systematic_type_tag
    3.48 +      | _ => metis_ad_hoc_type_tag, true))]
    3.49  
    3.50  fun old_skolem_const_name i j num_T_args =
    3.51    old_skolem_const_prefix ^ Long_Name.separator ^
    3.52 @@ -114,32 +119,34 @@
    3.53  val prepare_helper =
    3.54    Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
    3.55  
    3.56 -fun metis_term_from_atp (ATerm (s, tms)) =
    3.57 +fun metis_term_from_atp type_enc (ATerm (s, tms)) =
    3.58    if is_tptp_variable s then
    3.59      Metis_Term.Var (Metis_Name.fromString s)
    3.60    else
    3.61 -    let
    3.62 -      val (s, swap) = AList.lookup (op =) metis_name_table (s, length tms)
    3.63 -                      |> the_default (s, false)
    3.64 -    in
    3.65 -      Metis_Term.Fn (Metis_Name.fromString s,
    3.66 -                     tms |> map metis_term_from_atp |> swap ? rev)
    3.67 -    end
    3.68 -fun metis_atom_from_atp (AAtom tm) =
    3.69 -    (case metis_term_from_atp tm of
    3.70 +    (case AList.lookup (op =) metis_name_table (s, length tms) of
    3.71 +       SOME (f, swap) => (f type_enc, swap)
    3.72 +     | NONE => (s, false))
    3.73 +    |> (fn (s, swap) =>
    3.74 +           Metis_Term.Fn (Metis_Name.fromString s,
    3.75 +                          tms |> map (metis_term_from_atp type_enc)
    3.76 +                              |> swap ? rev))
    3.77 +fun metis_atom_from_atp type_enc (AAtom tm) =
    3.78 +    (case metis_term_from_atp type_enc tm of
    3.79         Metis_Term.Fn x => x
    3.80       | _ => raise Fail "non CNF -- expected function")
    3.81 -  | metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
    3.82 -fun metis_literal_from_atp (AConn (ANot, [phi])) =
    3.83 -    (false, metis_atom_from_atp phi)
    3.84 -  | metis_literal_from_atp phi = (true, metis_atom_from_atp phi)
    3.85 -fun metis_literals_from_atp (AConn (AOr, phis)) =
    3.86 -    maps metis_literals_from_atp phis
    3.87 -  | metis_literals_from_atp phi = [metis_literal_from_atp phi]
    3.88 -fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
    3.89 +  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
    3.90 +fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
    3.91 +    (false, metis_atom_from_atp type_enc phi)
    3.92 +  | metis_literal_from_atp type_enc phi =
    3.93 +    (true, metis_atom_from_atp type_enc phi)
    3.94 +fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
    3.95 +    maps (metis_literals_from_atp type_enc) phis
    3.96 +  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
    3.97 +fun metis_axiom_from_atp type_enc clauses (Formula (ident, _, phi, _, _)) =
    3.98      let
    3.99        fun some isa =
   3.100 -        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
   3.101 +        SOME (phi |> metis_literals_from_atp type_enc
   3.102 +                  |> Metis_LiteralSet.fromList
   3.103                    |> Metis_Thm.axiom, isa)
   3.104      in
   3.105        if ident = type_tag_idempotence_helper_name orelse
   3.106 @@ -164,7 +171,7 @@
   3.107          in Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some end
   3.108        | NONE => TrueI |> Isa_Raw |> some
   3.109      end
   3.110 -  | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
   3.111 +  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
   3.112  
   3.113  (* Function to generate metis clauses, including comb and type clauses *)
   3.114  fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
   3.115 @@ -205,8 +212,8 @@
   3.116      *)
   3.117      (* "rev" is for compatibility. *)
   3.118      val axioms =
   3.119 -      atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
   3.120 -                  |> rev
   3.121 +      atp_problem
   3.122 +      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
   3.123    in (sym_tab, axioms, old_skolems) end
   3.124  
   3.125  end;