1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 16:29:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:34 2011 +0200
     1.3 @@ -77,6 +77,7 @@
     1.4    val tfree_clause_prefix : string
     1.5    val typed_helper_suffix : string
     1.6    val untyped_helper_suffix : string
     1.7 +  val type_tag_idempotence_helper_name : string
     1.8    val predicator_name : string
     1.9    val app_op_name : string
    1.10    val type_tag_name : string
    1.11 @@ -87,7 +88,8 @@
    1.12    val ascii_of: string -> string
    1.13    val unascii_of: string -> string
    1.14    val strip_prefix_and_unascii : string -> string -> string option
    1.15 -  val proxify_const : string -> (int * (string * string)) option
    1.16 +  val proxy_table : (string * (string * (thm * (string * string)))) list
    1.17 +  val proxify_const : string -> (string * string) option
    1.18    val invert_const: string -> string
    1.19    val unproxify_const: string -> string
    1.20    val make_bound_var : string -> string
    1.21 @@ -125,6 +127,7 @@
    1.22      Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
    1.23      -> translated_formula option * ((string * locality) * thm)
    1.24    val helper_table : (string * (bool * thm list)) list
    1.25 +  val should_specialize_helper : type_sys -> term -> bool
    1.26    val tfree_classes_of_terms : term list -> string list
    1.27    val tvar_classes_of_terms : term list -> string list
    1.28    val type_consts_of_terms : theory -> term list -> string list
    1.29 @@ -183,12 +186,13 @@
    1.30  val fact_prefix = "fact_"
    1.31  val conjecture_prefix = "conj_"
    1.32  val helper_prefix = "help_"
    1.33 -val class_rel_clause_prefix = "crel_"
    1.34 +val class_rel_clause_prefix = "clar_"
    1.35  val arity_clause_prefix = "arity_"
    1.36  val tfree_clause_prefix = "tfree_"
    1.37  
    1.38  val typed_helper_suffix = "_T"
    1.39  val untyped_helper_suffix = "_U"
    1.40 +val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
    1.41  
    1.42  val predicator_name = "hBOOL"
    1.43  val app_op_name = "hAPP"
    1.44 @@ -257,19 +261,23 @@
    1.45    else
    1.46      NONE
    1.47  
    1.48 -val proxies =
    1.49 -  [("c_False",
    1.50 -    (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),
    1.51 -   ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),
    1.52 -   ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),
    1.53 -   ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),
    1.54 -   ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),
    1.55 -   ("c_implies",
    1.56 -    (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),
    1.57 -   ("equal",
    1.58 -    (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]
    1.59 +val proxy_table =
    1.60 +  [("c_False", (@{const_name False}, (@{thm fFalse_def},
    1.61 +       ("fFalse", @{const_name ATP.fFalse})))),
    1.62 +   ("c_True", (@{const_name True}, (@{thm fTrue_def},
    1.63 +       ("fTrue", @{const_name ATP.fTrue})))),
    1.64 +   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
    1.65 +       ("fNot", @{const_name ATP.fNot})))),
    1.66 +   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
    1.67 +       ("fconj", @{const_name ATP.fconj})))),
    1.68 +   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
    1.69 +       ("fdisj", @{const_name ATP.fdisj})))),
    1.70 +   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
    1.71 +       ("fimplies", @{const_name ATP.fimplies})))),
    1.72 +   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
    1.73 +       ("fequal", @{const_name ATP.fequal}))))]
    1.74  
    1.75 -val proxify_const = AList.lookup (op =) proxies #> Option.map snd
    1.76 +val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
    1.77  
    1.78  (* Readable names for the more common symbolic functions. Do not mess with the
    1.79     table unless you know what you are doing. *)
    1.80 @@ -291,14 +299,14 @@
    1.81     (@{const_name Meson.COMBC}, "COMBC"),
    1.82     (@{const_name Meson.COMBS}, "COMBS")]
    1.83    |> Symtab.make
    1.84 -  |> fold (Symtab.update o swap o snd o snd o snd) proxies
    1.85 +  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
    1.86  
    1.87  (* Invert the table of translations between Isabelle and ATPs. *)
    1.88  val const_trans_table_inv =
    1.89    const_trans_table |> Symtab.dest |> map swap |> Symtab.make
    1.90  val const_trans_table_unprox =
    1.91    Symtab.empty
    1.92 -  |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies
    1.93 +  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
    1.94  
    1.95  val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
    1.96  val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
    1.97 @@ -793,7 +801,7 @@
    1.98          CombApp (intro top_level tm1, intro false tm2)
    1.99        | intro top_level (CombConst (name as (s, _), T, T_args)) =
   1.100          (case proxify_const s of
   1.101 -           SOME (_, proxy_base) =>
   1.102 +           SOME proxy_base =>
   1.103             if top_level orelse is_setting_higher_order format type_sys then
   1.104               case (top_level, s) of
   1.105                 (_, "c_False") => (`I tptp_false, [])
   1.106 @@ -1284,52 +1292,57 @@
   1.107                      "~ fimplies P Q | ~ P | Q"
   1.108                  by (unfold fimplies_def) fast+})),
   1.109     ("If", (true, @{thms if_True if_False True_or_False}))]
   1.110 +  |> map (apsnd (apsnd (map zero_var_indexes)))
   1.111  
   1.112  val type_tag = `make_fixed_const type_tag_name
   1.113  
   1.114 -fun ti_ti_helper_fact () =
   1.115 +fun type_tag_idempotence_fact () =
   1.116    let
   1.117      fun var s = ATerm (`I s, [])
   1.118 -    fun tag tm = ATerm (type_tag, [var "X", tm])
   1.119 +    fun tag tm = ATerm (type_tag, [var "T", tm])
   1.120 +    val tagged_x = tag (var "X")
   1.121    in
   1.122 -    Formula (helper_prefix ^ "ti_ti", Axiom,
   1.123 -             AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
   1.124 +    Formula (type_tag_idempotence_helper_name, Axiom,
   1.125 +             AAtom (ATerm (`I tptp_equal, [tag tagged_x, tagged_x]))
   1.126               |> close_formula_universally, simp_info, NONE)
   1.127    end
   1.128  
   1.129 +fun should_specialize_helper type_sys t =
   1.130 +  case general_type_arg_policy type_sys of
   1.131 +    Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
   1.132 +  | _ => false
   1.133 +
   1.134  fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
   1.135    case strip_prefix_and_unascii const_prefix s of
   1.136      SOME mangled_s =>
   1.137      let
   1.138        val thy = Proof_Context.theory_of ctxt
   1.139        val unmangled_s = mangled_s |> unmangled_const_name
   1.140 -      fun dub_and_inst c needs_fairly_sound (th, j) =
   1.141 -        ((c ^ "_" ^ string_of_int j ^
   1.142 +      fun dub_and_inst needs_fairly_sound (th, j) =
   1.143 +        ((unmangled_s ^ "_" ^ string_of_int j ^
   1.144 +          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
   1.145            (if needs_fairly_sound then typed_helper_suffix
   1.146             else untyped_helper_suffix),
   1.147            General),
   1.148           let val t = th |> prop_of in
   1.149 -           t |> ((case general_type_arg_policy type_sys of
   1.150 -                    Mangled_Type_Args _ => true
   1.151 -                  | _ => false) andalso
   1.152 -                 not (null (Term.hidden_polymorphism t)))
   1.153 +           t |> should_specialize_helper type_sys t
   1.154                  ? (case types of
   1.155                       [T] => specialize_type thy (invert_const unmangled_s, T)
   1.156                     | _ => I)
   1.157           end)
   1.158 -      fun make_facts eq_as_iff =
   1.159 -        map_filter (make_fact ctxt format type_sys true false eq_as_iff false)
   1.160 +      val make_facts =
   1.161 +        map_filter (make_fact ctxt format type_sys false false false false)
   1.162        val fairly_sound = is_type_sys_fairly_sound type_sys
   1.163      in
   1.164        helper_table
   1.165 -      |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
   1.166 -                  if metis_s <> unmangled_s orelse
   1.167 +      |> maps (fn (helper_s, (needs_fairly_sound, ths)) =>
   1.168 +                  if helper_s <> unmangled_s orelse
   1.169                       (needs_fairly_sound andalso not fairly_sound) then
   1.170                      []
   1.171                    else
   1.172                      ths ~~ (1 upto length ths)
   1.173 -                    |> map (dub_and_inst mangled_s needs_fairly_sound)
   1.174 -                    |> make_facts (not needs_fairly_sound))
   1.175 +                    |> map (dub_and_inst needs_fairly_sound)
   1.176 +                    |> make_facts)
   1.177      end
   1.178    | NONE => []
   1.179  fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
   1.180 @@ -1509,11 +1522,14 @@
   1.181  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
   1.182     of monomorphization). The TPTP explicitly forbids name clashes, and some of
   1.183     the remote provers might care. *)
   1.184 -fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
   1.185 +fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
   1.186                            (j, formula as {name, locality, kind, ...}) =
   1.187 -  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
   1.188 -                     else string_of_int j ^ "_") ^
   1.189 -           ascii_of name,
   1.190 +  Formula (prefix ^
   1.191 +           (if freshen andalso
   1.192 +               polymorphism_of_type_sys type_sys <> Polymorphic then
   1.193 +              string_of_int j ^ "_"
   1.194 +            else
   1.195 +              "") ^ encode name,
   1.196             kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
   1.197             case locality of
   1.198               Intro => intro_info
   1.199 @@ -1774,9 +1790,9 @@
   1.200    |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
   1.201                                                       nonmono_Ts type_sys)
   1.202  
   1.203 -fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavyweight)) =
   1.204 +fun needs_type_tag_idempotence (Tags (Polymorphic, level, Heavyweight)) =
   1.205      level = Nonmonotonic_Types orelse level = Finite_Types
   1.206 -  | should_add_ti_ti_helper _ = false
   1.207 +  | needs_type_tag_idempotence _ = false
   1.208  
   1.209  fun offset_of_heading_in_problem _ [] j = j
   1.210    | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
   1.211 @@ -1822,16 +1838,19 @@
   1.212                                            lavish_nonmono_Ts type_sys
   1.213      val helper_lines =
   1.214        0 upto length helpers - 1 ~~ helpers
   1.215 -      |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
   1.216 -                                    type_sys)
   1.217 -      |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
   1.218 -          else I)
   1.219 +      |> map (formula_line_for_fact ctxt format helper_prefix I false
   1.220 +                                    lavish_nonmono_Ts type_sys)
   1.221 +      |> (if needs_type_tag_idempotence type_sys then
   1.222 +            cons (type_tag_idempotence_fact ())
   1.223 +          else
   1.224 +            I)
   1.225      (* Reordering these might confuse the proof reconstruction code or the SPASS
   1.226         FLOTTER hack. *)
   1.227      val problem =
   1.228        [(explicit_declsN, sym_decl_lines),
   1.229         (factsN,
   1.230 -        map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
   1.231 +        map (formula_line_for_fact ctxt format fact_prefix ascii_of true
   1.232 +                                   nonmono_Ts type_sys)
   1.233              (0 upto length facts - 1 ~~ facts)),
   1.234         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   1.235         (aritiesN, map formula_line_for_arity_clause arity_clauses),

     2.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 16:29:38 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
     2.3 @@ -17,8 +17,8 @@
     2.4    val trace_msg : Proof.context -> (unit -> string) -> unit
     2.5    val verbose : bool Config.T
     2.6    val verbose_warning : Proof.context -> string -> unit
     2.7 -  val hol_clause_from_metis_MX :
     2.8 -    Proof.context -> int Symtab.table -> Metis_Literal.literal list -> term
     2.9 +  val hol_clause_from_metis :
    2.10 +    Proof.context -> int Symtab.table -> Metis_Thm.thm -> term
    2.11    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    2.12    val untyped_aconv : term * term -> bool
    2.13    val replay_one_inference :
    2.14 @@ -236,8 +236,11 @@
    2.15    | atp_clause_from_metis lits =
    2.16      lits |> map atp_literal_from_metis |> mk_aconns AOr
    2.17  
    2.18 -fun hol_clause_from_metis_MX ctxt sym_tab =
    2.19 -  atp_clause_from_metis #> prop_from_atp ctxt false sym_tab
    2.20 +fun hol_clause_from_metis ctxt sym_tab =
    2.21 +  Metis_Thm.clause
    2.22 +  #> Metis_LiteralSet.toList
    2.23 +  #> atp_clause_from_metis
    2.24 +  #> prop_from_atp ctxt false sym_tab
    2.25  
    2.26  fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
    2.27    let val ts = map (hol_term_from_metis ctxt mode sym_tab) fol_tms

     3.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 16:29:38 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:34 2011 +0200
     3.3 @@ -46,8 +46,6 @@
     3.4  val new_skolemizer =
     3.5    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
     3.6  
     3.7 -fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
     3.8 -
     3.9  (* Designed to work also with monomorphic instances of polymorphic theorems. *)
    3.10  fun have_common_thm ths1 ths2 =
    3.11    exists (member (untyped_aconv o pairself prop_of) ths1)
    3.12 @@ -60,11 +58,10 @@
    3.13  (* Lightweight predicate type information comes in two flavors, "t = t'" and
    3.14     "t => t'", where "t" and "t'" are the same term modulo type tags.
    3.15     In Isabelle, type tags are stripped away, so we are left with "t = t" or
    3.16 -   "t => t". *)
    3.17 -fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth =
    3.18 +   "t => t". Type tag idempotence is also handled this way. *)
    3.19 +fun reflexive_or_trivial_from_metis ctxt sym_tab mth =
    3.20    let val thy = Proof_Context.theory_of ctxt in
    3.21 -    case hol_clause_from_metis_MX ctxt sym_tab
    3.22 -             (Metis_LiteralSet.toList (Metis_Thm.clause mth)) of
    3.23 +    case hol_clause_from_metis ctxt sym_tab mth of
    3.24        Const (@{const_name HOL.eq}, _) $ _ $ t =>
    3.25        t |> cterm_of thy |> Thm.reflexive RS @{thm meta_eq_to_obj_eq}
    3.26      | Const (@{const_name disj}, _) $ t1 $ t2 =>
    3.27 @@ -74,6 +71,9 @@
    3.28    end
    3.29    |> Meson.make_meta_clause
    3.30  
    3.31 +(* FIXME: implement using "hol_clause_from_metis ctxt sym_tab mth" *)
    3.32 +fun specialize_helper mth ith = ith
    3.33 +
    3.34  val clause_params =
    3.35    {ordering = Metis_KnuthBendixOrder.default,
    3.36     orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    3.37 @@ -107,19 +107,21 @@
    3.38        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    3.39        val (mode, sym_tab, {axioms, old_skolems, ...}) =
    3.40          prepare_metis_problem ctxt mode type_sys cls ths
    3.41 -      val axioms =
    3.42 -        axioms |> map
    3.43 -            (fn (mth, SOME th) => (mth, th)
    3.44 -              | (mth, NONE) =>
    3.45 -                (mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth))
    3.46 +      fun get_isa_thm mth Isa_Reflexive_or_Trivial =
    3.47 +          reflexive_or_trivial_from_metis ctxt sym_tab mth
    3.48 +        | get_isa_thm mth (Isa_Helper ith) =
    3.49 +          ith |> should_specialize_helper (the type_sys) (prop_of ith)
    3.50 +                 ? specialize_helper mth
    3.51 +        | get_isa_thm _ (Isa_Raw ith) = ith
    3.52 +      val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
    3.53        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    3.54 -      val thms = map #1 axioms
    3.55 +      val thms = axioms |> map fst
    3.56        val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    3.57        val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
    3.58        val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    3.59    in
    3.60 -      case filter (is_false o prop_of) cls of
    3.61 -          false_th::_ => [false_th RS @{thm FalseE}]
    3.62 +      case filter (fn t => prop_of t aconv @{prop False}) cls of
    3.63 +          false_th :: _ => [false_th RS @{thm FalseE}]
    3.64          | [] =>
    3.65        case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    3.66             |> Metis_Resolution.loop of

     4.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 16:29:38 2011 +0200
     4.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:34 2011 +0200
     4.3 @@ -14,8 +14,13 @@
     4.4  
     4.5    datatype mode = FO | HO | FT | MX
     4.6  
     4.7 +  datatype isa_thm =
     4.8 +    Isa_Reflexive_or_Trivial |
     4.9 +    Isa_Helper of thm |
    4.10 +    Isa_Raw of thm
    4.11 +
    4.12    type metis_problem =
    4.13 -    {axioms : (Metis_Thm.thm * thm option) list,
    4.14 +    {axioms : (Metis_Thm.thm * isa_thm) list,
    4.15       tfrees : type_literal list,
    4.16       old_skolems : (string * term) list}
    4.17  
    4.18 @@ -235,8 +240,13 @@
    4.19  (* Logic maps manage the interface between HOL and first-order logic.        *)
    4.20  (* ------------------------------------------------------------------------- *)
    4.21  
    4.22 +datatype isa_thm =
    4.23 +  Isa_Reflexive_or_Trivial |
    4.24 +  Isa_Helper of thm |
    4.25 +  Isa_Raw of thm
    4.26 +
    4.27  type metis_problem =
    4.28 -  {axioms : (Metis_Thm.thm * thm option) list,
    4.29 +  {axioms : (Metis_Thm.thm * isa_thm) list,
    4.30     tfrees : type_literal list,
    4.31     old_skolems : (string * term) list}
    4.32  
    4.33 @@ -285,6 +295,10 @@
    4.34      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    4.35    in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
    4.36  
    4.37 +val proxy_defs = map (fst o snd o snd) proxy_table
    4.38 +val prepare_helper =
    4.39 +  Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
    4.40 +
    4.41  fun metis_name_from_atp s ary =
    4.42    AList.lookup (op =) metis_name_table (s, ary) |> the_default (s, false)
    4.43  fun metis_term_from_atp (ATerm (s, tms)) =
    4.44 @@ -308,18 +322,23 @@
    4.45  fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
    4.46      (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
    4.47           |> Metis_Thm.axiom,
    4.48 -     case try (unprefix conjecture_prefix) ident of
    4.49 +     if ident = type_tag_idempotence_helper_name orelse
    4.50 +        String.isPrefix lightweight_tags_sym_formula_prefix ident then
    4.51 +       Isa_Reflexive_or_Trivial
    4.52 +     else if String.isPrefix helper_prefix ident then
    4.53 +       case space_explode "_" ident  of
    4.54 +         _ :: const :: j :: _ =>
    4.55 +         Isa_Helper (nth (AList.lookup (op =) helper_table const |> the |> snd)
    4.56 +                         (the (Int.fromString j) - 1)
    4.57 +                     |> prepare_helper)
    4.58 +       | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    4.59 +     else case try (unprefix conjecture_prefix) ident of
    4.60         SOME s =>
    4.61 -       SOME (Meson.make_meta_clause (nth clauses (the (Int.fromString s))))
    4.62 -     | NONE =>
    4.63 -       if String.isPrefix lightweight_tags_sym_formula_prefix ident then
    4.64 -         NONE
    4.65 -(* FIXME: missing:
    4.66 -       else if String.isPrefix helper_prefix then
    4.67 -         ...
    4.68 -*)
    4.69 -       else
    4.70 -         SOME TrueI)
    4.71 +       let val j = the (Int.fromString s) in
    4.72 +         Isa_Raw (if j = length clauses then TrueI
    4.73 +                  else Meson.make_meta_clause (nth clauses j))
    4.74 +       end
    4.75 +     | NONE => Isa_Raw TrueI)
    4.76    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    4.77  
    4.78  val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
    4.79 @@ -342,8 +361,7 @@
    4.80          prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
    4.81                              false false (map prop_of clauses) @{prop False} []
    4.82        val axioms =
    4.83 -        atp_problem
    4.84 -        |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
    4.85 +        atp_problem |> maps (map (metis_axiom_from_atp clauses) o snd)
    4.86      in
    4.87        (MX, sym_tab,
    4.88         {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
    4.89 @@ -366,14 +384,14 @@
    4.90              hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
    4.91                             metis_ith
    4.92          in
    4.93 -          {axioms = (mth, SOME isa_ith) :: axioms,
    4.94 +          {axioms = (mth, Isa_Raw isa_ith) :: axioms,
    4.95             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
    4.96          end;
    4.97        fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
    4.98 -        {axioms = (mth, SOME ith) :: axioms, tfrees = tfrees,
    4.99 +        {axioms = (mth, Isa_Raw ith) :: axioms, tfrees = tfrees,
   4.100           old_skolems = old_skolems}
   4.101        fun add_tfrees {axioms, tfrees, old_skolems} =
   4.102 -        {axioms = map (rpair (SOME TrueI) o metis_of_tfree)
   4.103 +        {axioms = map (rpair (Isa_Raw TrueI) o metis_of_tfree)
   4.104                        (distinct (op =) tfrees) @ axioms,
   4.105           tfrees = tfrees, old_skolems = old_skolems}
   4.106        val problem =
   4.107 @@ -389,18 +407,12 @@
   4.108            problem
   4.109          else
   4.110            let
   4.111 -            val fdefs = @{thms fFalse_def fTrue_def fNot_def fconj_def fdisj_def
   4.112 -                               fimplies_def fequal_def}
   4.113 -            val prepare_helper =
   4.114 -              zero_var_indexes
   4.115 -              #> `(Meson.make_meta_clause
   4.116 -                   #> rewrite_rule (map safe_mk_meta_eq fdefs))
   4.117              val helper_ths =
   4.118                helper_table
   4.119                |> filter (is_used o prefix const_prefix o fst)
   4.120                |> maps (fn (_, (needs_full_types, thms)) =>
   4.121                            if needs_full_types andalso mode <> FT then []
   4.122 -                          else map prepare_helper thms)
   4.123 +                          else map (`prepare_helper) thms)
   4.124            in problem |> fold (add_thm false) helper_ths end
   4.125        val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
   4.126      in (mode, Symtab.empty, fold add_type_thm type_ths problem) end