1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue May 31 16:38:36 2011 +0200
     1.3 @@ -222,15 +222,16 @@
     1.4      ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms)
     1.5    | atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
     1.6  
     1.7 -fun hol_term_from_metis_New sym_tab ctxt =
     1.8 +fun hol_term_from_metis_MX sym_tab ctxt =
     1.9    let val thy = Proof_Context.theory_of ctxt in
    1.10 -    atp_term_from_metis #> term_from_atp thy false sym_tab [](*###tfrees*) NONE
    1.11 +    atp_term_from_metis #> term_from_atp thy false sym_tab []
    1.12 +    (* FIXME ### tfrees instead of []? *) NONE
    1.13    end
    1.14  
    1.15  fun hol_term_from_metis FO _ = hol_term_from_metis_PT
    1.16    | hol_term_from_metis HO _ = hol_term_from_metis_PT
    1.17    | hol_term_from_metis FT _ = hol_term_from_metis_FT
    1.18 -  | hol_term_from_metis New sym_tab = hol_term_from_metis_New sym_tab
    1.19 +  | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
    1.20  
    1.21  fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
    1.22    let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
    1.23 @@ -524,13 +525,13 @@
    1.24                        space_implode " " (map string_of_int ps) ^
    1.25                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
    1.26                        " fol-term: " ^ Metis_Term.toString t)
    1.27 -      fun path_finder_New tm [] _ = (tm, Bound 0)
    1.28 -        | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
    1.29 +      fun path_finder_MX tm [] _ = (tm, Bound 0)
    1.30 +        | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
    1.31            if s = metis_app_op (* FIXME ### mangled etc. *) then
    1.32              let
    1.33                val (tm1, tm2) = dest_comb tm in
    1.34 -              if p = 0 then path_finder_New tm1 ps (hd ts) ||> (fn y => y $ tm2)
    1.35 -              else path_finder_New tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
    1.36 +              if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)
    1.37 +              else path_finder_MX tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
    1.38              end
    1.39            else
    1.40              let
    1.41 @@ -546,11 +547,11 @@
    1.42                val _ = trace_msg ctxt (fn () =>
    1.43                    "path_finder: " ^ string_of_int p ^ "  " ^
    1.44                    Syntax.string_of_term ctxt tm_p)
    1.45 -              val (r, t) = path_finder_New tm_p ps (nth ts p)
    1.46 +              val (r, t) = path_finder_MX tm_p ps (nth ts p)
    1.47              in (r, list_comb (tm1, replace_item_list t p' args)) end
    1.48 -        | path_finder_New tm ps t =
    1.49 +        | path_finder_MX tm ps t =
    1.50            raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
    1.51 -                      "equality_inf, path_finder_New: path = " ^
    1.52 +                      "equality_inf, path_finder_MX: path = " ^
    1.53                        space_implode " " (map string_of_int ps) ^
    1.54                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
    1.55                        " fol-term: " ^ Metis_Term.toString t)
    1.56 @@ -573,7 +574,7 @@
    1.57          | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
    1.58               (*if not equality, ignore head to skip the hBOOL predicate*)
    1.59          | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
    1.60 -        | path_finder New tm ps t = path_finder_New tm ps t
    1.61 +        | path_finder MX tm ps t = path_finder_MX tm ps t
    1.62        fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
    1.63              let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
    1.64              in (tm, nt $ tm_rslt) end

     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue May 31 16:38:36 2011 +0200
     2.3 @@ -36,12 +36,12 @@
     2.4  fun method_binding_for_mode HO = @{binding metis}
     2.5    | method_binding_for_mode FO = @{binding metisF}
     2.6    | method_binding_for_mode FT = @{binding metisFT}
     2.7 -  | method_binding_for_mode New = @{binding metisX}
     2.8 +  | method_binding_for_mode MX = @{binding metisX}
     2.9  
    2.10  val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
    2.11  val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
    2.12  val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
    2.13 -val metisX_N = Binding.qualified_name_of (method_binding_for_mode New)
    2.14 +val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX)
    2.15  
    2.16  val new_skolemizer =
    2.17    Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
    2.18 @@ -184,7 +184,7 @@
    2.19  val metisF_modes = [FO, FT]
    2.20  val metisFT_modes = [FT]
    2.21  val metisHO_modes = [HO]
    2.22 -val metisX_modes = [New]
    2.23 +val metisX_modes = [MX]
    2.24  
    2.25  val metis_tac = generic_metis_tac metis_modes NONE
    2.26  val metisF_tac = generic_metis_tac metisF_modes NONE
    2.27 @@ -212,7 +212,7 @@
    2.28  
    2.29  fun setup_method (modes as mode :: _) =
    2.30    Method.setup (method_binding_for_mode mode)
    2.31 -               ((if mode = New then
    2.32 +               ((if mode = MX then
    2.33                     Scan.lift (Scan.option (Args.parens Parse.short_ident))
    2.34                   else
    2.35                     Scan.succeed NONE)

     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue May 31 16:38:36 2011 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4    type type_literal = ATP_Translate.type_literal
     3.5    type type_sys = ATP_Translate.type_sys
     3.6  
     3.7 -  datatype mode = FO | HO | FT | New
     3.8 +  datatype mode = FO | HO | FT | MX
     3.9  
    3.10    type metis_problem =
    3.11      {axioms : (Metis_Thm.thm * thm) list,
    3.12 @@ -111,13 +111,13 @@
    3.13  (* HOL to FOL  (Isabelle to Metis)                                           *)
    3.14  (* ------------------------------------------------------------------------- *)
    3.15  
    3.16 -(* first-order, higher-order, fully-typed, new *)
    3.17 -datatype mode = FO | HO | FT | New
    3.18 +(* first-order, higher-order, fully-typed, mode X (fleXible) *)
    3.19 +datatype mode = FO | HO | FT | MX
    3.20  
    3.21  fun string_of_mode FO = "FO"
    3.22    | string_of_mode HO = "HO"
    3.23    | string_of_mode FT = "FT"
    3.24 -  | string_of_mode New = "New"
    3.25 +  | string_of_mode MX = "MX"
    3.26  
    3.27  fun fn_isa_to_met_sublevel "equal" = "c_fequal"
    3.28    | fn_isa_to_met_sublevel "c_False" = "c_fFalse"
    3.29 @@ -310,7 +310,7 @@
    3.30  val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light)
    3.31  
    3.32  (* Function to generate metis clauses, including comb and type clauses *)
    3.33 -fun prepare_metis_problem ctxt New type_sys conj_clauses fact_clauses =
    3.34 +fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
    3.35      let
    3.36        val type_sys = type_sys |> the_default default_type_sys
    3.37        val explicit_apply = NONE
    3.38 @@ -322,7 +322,7 @@
    3.39          atp_problem
    3.40          |> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
    3.41      in
    3.42 -      (New, sym_tab,
    3.43 +      (MX, sym_tab,
    3.44         {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
    3.45      end
    3.46    | prepare_metis_problem ctxt mode _ conj_clauses fact_clauses =