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