src/HOL/Tools/Metis/metis_tactic.ML

 
 (* Lightweight predicate type information comes in two flavors, "t = t'" and
    "t => t'", where "t" and "t'" are the same term modulo type tags.
    In Isabelle, type tags are stripped away, so we are left with "t = t" or
    "t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
+fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
   let val thy = Proof_Context.theory_of ctxt in
-    case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
+    case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
       Const (@{const_name HOL.eq}, _) $ _ $ t =>
       let
         val ct = cterm_of thy t
         val cT = ctyp_of_term ct
       in refl |> Drule.instantiate' [SOME cT] [SOME ct] end

       |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial
     | _ => raise Fail "expected reflexive or trivial clause"
   end
   |> Meson.make_meta_clause
 
-fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
+fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
   let
     val thy = Proof_Context.theory_of ctxt
     val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
-    val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
+    val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
 
 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t

       val dischargers = map (fst o snd) th_cls_pairs
       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
       val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
-      val type_enc = type_enc_from_string Strict type_enc
+      val type_enc = type_enc_of_string Strict type_enc
       val (sym_tab, axioms, ord_info, concealed) =
         prepare_metis_problem ctxt type_enc lam_trans cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
-          reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
+          reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
         | get_isa_thm mth Isa_Lambda_Lifted =
-          lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
+          lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
         | get_isa_thm _ (Isa_Raw ith) = ith
       val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
       val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
       val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms
       val _ = trace_msg ctxt (fn () => "METIS CLAUSES")