tuning -- renamed '_from_' to '_of_' in Sledgehammer
authorblanchet
Thu May 16 13:34:13 2013 +0200 (2013-05-16 ago)
changeset 520319a9238342963
parent 52030 9f6f0a89d16b
child 52032 0370c5f00ce8
tuning -- renamed '_from_' to '_of_' in Sledgehammer
src/HOL/BNF/Tools/bnf_fp_util.ML
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 16 13:19:27 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 16 13:34:13 2013 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  val timing = true;
     1.6  fun time timer msg = (if timing
     1.7 -  then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
     1.8 +  then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
     1.9    else (); Timer.startRealTimer ());
    1.10  
    1.11  val preN = "pre_"
     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Thu May 16 13:19:27 2013 +0200
     2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Thu May 16 13:34:13 2013 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4  
     2.5  fun refute_tptp_file thy timeout file_name =
     2.6    let
     2.7 -    fun print_szs_from_outcome falsify s =
     2.8 +    fun print_szs_of_outcome falsify s =
     2.9        "% SZS status " ^
    2.10        (if s = "genuine" then
    2.11           if falsify then "CounterSatisfiable" else "Satisfiable"
    2.12 @@ -122,7 +122,7 @@
    2.13    in
    2.14      Refute.refute_term ctxt params (defs @ nondefs)
    2.15          (case conjs of conj :: _ => conj | [] => @{prop True})
    2.16 -    |> print_szs_from_outcome (not (null conjs))
    2.17 +    |> print_szs_of_outcome (not (null conjs))
    2.18    end
    2.19  
    2.20  
    2.21 @@ -263,7 +263,7 @@
    2.22    Logic.list_implies (rev defs @ rev nondefs,
    2.23                        case conjs of conj :: _ => conj | [] => @{prop False})
    2.24  
    2.25 -fun print_szs_from_success conjs success =
    2.26 +fun print_szs_of_success conjs success =
    2.27    Output.urgent_message ("% SZS status " ^
    2.28                           (if success then
    2.29                              if null conjs then "Unsatisfiable" else "Theorem"
    2.30 @@ -277,7 +277,7 @@
    2.31      val conj = make_conj assms conjs
    2.32    in
    2.33      can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
    2.34 -    |> print_szs_from_success conjs
    2.35 +    |> print_szs_of_success conjs
    2.36    end
    2.37  
    2.38  fun generic_isabelle_tptp_file demo thy timeout file_name =
    2.39 @@ -292,7 +292,7 @@
    2.40       can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
    2.41       can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
    2.42           (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
    2.43 -    |> print_szs_from_success conjs
    2.44 +    |> print_szs_of_success conjs
    2.45    end
    2.46  
    2.47  val isabelle_tptp_file = generic_isabelle_tptp_file false
     3.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:19:27 2013 +0200
     3.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:34:13 2013 +0200
     3.3 @@ -157,7 +157,7 @@
     3.4    let
     3.5      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     3.6      val type_enc =
     3.7 -      type_enc |> type_enc_from_string Non_Strict
     3.8 +      type_enc |> type_enc_of_string Non_Strict
     3.9                 |> adjust_type_enc format
    3.10      val mono = not (is_type_enc_polymorphic type_enc)
    3.11      val facts =
     4.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu May 16 13:19:27 2013 +0200
     4.2 +++ b/src/HOL/TPTP/mash_eval.ML	Thu May 16 13:34:13 2013 +0200
     4.3 @@ -75,7 +75,7 @@
     4.4        let val facts = facts |> map (fst o fst) in
     4.5          str_of_method method ^
     4.6          (if is_none outcome then
     4.7 -           "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
     4.8 +           "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
     4.9             (used_facts |> map (with_index facts o fst)
    4.10                         |> sort (int_ord o pairself fst)
    4.11                         |> map index_str
    4.12 @@ -199,7 +199,7 @@
    4.13         "slice" |> not slice ? prefix "dont_",
    4.14         "type_enc = " ^ the_default "smart" type_enc,
    4.15         "lam_trans = " ^ the_default "smart" lam_trans,
    4.16 -       "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout),
    4.17 +       "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
    4.18         "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
    4.19      val _ = print " * * *";
    4.20      val _ = print ("Options: " ^ commas options);
     5.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:19:27 2013 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:34:13 2013 +0200
     5.3 @@ -87,7 +87,7 @@
     5.4    val proxify_const : string -> (string * string) option
     5.5    val invert_const : string -> string
     5.6    val unproxify_const : string -> string
     5.7 -  val new_skolem_var_name_from_const : string -> string
     5.8 +  val new_skolem_var_name_of_const : string -> string
     5.9    val atp_logical_consts : string list
    5.10    val atp_irrelevant_consts : string list
    5.11    val atp_widely_irrelevant_consts : string list
    5.12 @@ -96,7 +96,7 @@
    5.13    val is_type_enc_polymorphic : type_enc -> bool
    5.14    val level_of_type_enc : type_enc -> type_level
    5.15    val is_type_enc_sound : type_enc -> bool
    5.16 -  val type_enc_from_string : strictness -> string -> type_enc
    5.17 +  val type_enc_of_string : strictness -> string -> type_enc
    5.18    val adjust_type_enc : atp_format -> type_enc -> type_enc
    5.19    val is_lambda_free : term -> bool
    5.20    val mk_aconns :
    5.21 @@ -104,7 +104,7 @@
    5.22    val unmangled_const : string -> string * (string, 'b) ho_term list
    5.23    val unmangled_const_name : string -> string list
    5.24    val helper_table : ((string * bool) * (status * thm) list) list
    5.25 -  val trans_lams_from_string :
    5.26 +  val trans_lams_of_string :
    5.27      Proof.context -> type_enc -> string -> term list -> term list * term list
    5.28    val string_of_status : status -> string
    5.29    val factsN : string
    5.30 @@ -395,7 +395,7 @@
    5.31  
    5.32  fun make_class clas = class_prefix ^ ascii_of clas
    5.33  
    5.34 -fun new_skolem_var_name_from_const s =
    5.35 +fun new_skolem_var_name_of_const s =
    5.36    let val ss = s |> space_explode Long_Name.separator in
    5.37      nth ss (length ss - 2)
    5.38    end
    5.39 @@ -568,18 +568,18 @@
    5.40  
    5.41  (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
    5.42     Also accumulates sort infomation. *)
    5.43 -fun iterm_from_term thy type_enc bs (P $ Q) =
    5.44 +fun iterm_of_term thy type_enc bs (P $ Q) =
    5.45      let
    5.46 -      val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
    5.47 -      val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
    5.48 +      val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
    5.49 +      val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
    5.50      in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
    5.51 -  | iterm_from_term thy type_enc _ (Const (c, T)) =
    5.52 +  | iterm_of_term thy type_enc _ (Const (c, T)) =
    5.53      (IConst (`(make_fixed_const (SOME type_enc)) c, T,
    5.54               robust_const_type_args thy (c, T)),
    5.55       atomic_types_of T)
    5.56 -  | iterm_from_term _ _ _ (Free (s, T)) =
    5.57 +  | iterm_of_term _ _ _ (Free (s, T)) =
    5.58      (IConst (`make_fixed_var s, T, []), atomic_types_of T)
    5.59 -  | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
    5.60 +  | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
    5.61      (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
    5.62         let
    5.63           val Ts = T |> strip_type |> swap |> op ::
    5.64 @@ -587,15 +587,14 @@
    5.65         in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
    5.66       else
    5.67         IVar ((make_schematic_var v, s), T), atomic_types_of T)
    5.68 -  | iterm_from_term _ _ bs (Bound j) =
    5.69 +  | iterm_of_term _ _ bs (Bound j) =
    5.70      nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
    5.71 -  | iterm_from_term thy type_enc bs (Abs (s, T, t)) =
    5.72 +  | iterm_of_term thy type_enc bs (Abs (s, T, t)) =
    5.73      let
    5.74        fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
    5.75        val s = vary s
    5.76        val name = `make_bound_var s
    5.77 -      val (tm, atomic_Ts) =
    5.78 -        iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
    5.79 +      val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
    5.80      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
    5.81  
    5.82  (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
    5.83 @@ -605,7 +604,7 @@
    5.84  fun try_unsuffixes ss s =
    5.85    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    5.86  
    5.87 -fun type_enc_from_string strictness s =
    5.88 +fun type_enc_of_string strictness s =
    5.89    (case try (unprefix "tc_") s of
    5.90       SOME s => (SOME Type_Class_Polymorphic, s)
    5.91     | NONE =>
    5.92 @@ -903,7 +902,7 @@
    5.93  val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
    5.94  val fused_infinite_type = Type (fused_infinite_type_name, [])
    5.95  
    5.96 -fun raw_ho_type_from_typ type_enc =
    5.97 +fun raw_ho_type_of_typ type_enc =
    5.98    let
    5.99      fun term (Type (s, Ts)) =
   5.100        AType (case (is_type_enc_higher_order type_enc, s) of
   5.101 @@ -919,11 +918,12 @@
   5.102      | term (TVar z) = AType (tvar_name z, [])
   5.103    in term end
   5.104  
   5.105 -fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
   5.106 -  | ho_term_from_ho_type _ = raise Fail "unexpected type"
   5.107 +fun ho_term_of_ho_type (AType (name, tys)) =
   5.108 +    ATerm ((name, []), map ho_term_of_ho_type tys)
   5.109 +  | ho_term_of_ho_type _ = raise Fail "unexpected type"
   5.110  
   5.111  fun ho_type_of_type_arg type_enc T =
   5.112 -  if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T)
   5.113 +  if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T)
   5.114  
   5.115  (* This shouldn't clash with anything else. *)
   5.116  val uncurried_alias_sep = "\000"
   5.117 @@ -938,7 +938,7 @@
   5.118    | generic_mangled_type_name _ _ = raise Fail "unexpected type"
   5.119  
   5.120  fun mangled_type type_enc =
   5.121 -  generic_mangled_type_name fst o raw_ho_type_from_typ type_enc
   5.122 +  generic_mangled_type_name fst o raw_ho_type_of_typ type_enc
   5.123  
   5.124  fun make_native_type s =
   5.125    if s = tptp_bool_type orelse s = tptp_fun_type orelse
   5.126 @@ -947,7 +947,7 @@
   5.127    else
   5.128      native_type_prefix ^ ascii_of s
   5.129  
   5.130 -fun native_ho_type_from_raw_ho_type type_enc pred_sym ary =
   5.131 +fun native_ho_type_of_raw_ho_type type_enc pred_sym ary =
   5.132    let
   5.133      fun to_mangled_atype ty =
   5.134        AType ((make_native_type (generic_mangled_type_name fst ty),
   5.135 @@ -967,9 +967,9 @@
   5.136        | to_ho _ = raise Fail "unexpected type"
   5.137    in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
   5.138  
   5.139 -fun native_ho_type_from_typ type_enc pred_sym ary =
   5.140 -  native_ho_type_from_raw_ho_type type_enc pred_sym ary
   5.141 -  o raw_ho_type_from_typ type_enc
   5.142 +fun native_ho_type_of_typ type_enc pred_sym ary =
   5.143 +  native_ho_type_of_raw_ho_type type_enc pred_sym ary
   5.144 +  o raw_ho_type_of_typ type_enc
   5.145  
   5.146  (* Make atoms for sorted type variables. *)
   5.147  fun generic_add_sorts_on_type _ [] = I
   5.148 @@ -983,9 +983,9 @@
   5.149  
   5.150  fun process_type_args type_enc T_args =
   5.151    if is_type_enc_native type_enc then
   5.152 -    (map (native_ho_type_from_typ type_enc false 0) T_args, [])
   5.153 +    (map (native_ho_type_of_typ type_enc false 0) T_args, [])
   5.154    else
   5.155 -    ([], map_filter (Option.map ho_term_from_ho_type
   5.156 +    ([], map_filter (Option.map ho_term_of_ho_type
   5.157                       o ho_type_of_type_arg type_enc) T_args)
   5.158  
   5.159  fun class_atom type_enc (cl, T) =
   5.160 @@ -1194,11 +1194,11 @@
   5.161        | filt _ tm = tm
   5.162    in filt 0 end
   5.163  
   5.164 -fun iformula_from_prop ctxt type_enc iff_for_eq =
   5.165 +fun iformula_of_prop ctxt type_enc iff_for_eq =
   5.166    let
   5.167      val thy = Proof_Context.theory_of ctxt
   5.168      fun do_term bs t atomic_Ts =
   5.169 -      iterm_from_term thy type_enc bs (Envir.eta_contract t)
   5.170 +      iterm_of_term thy type_enc bs (Envir.eta_contract t)
   5.171        |>> (introduce_proxies_in_iterm type_enc
   5.172             #> mangle_type_args_in_iterm type_enc #> AAtom)
   5.173        ||> union (op =) atomic_Ts
   5.174 @@ -1297,8 +1297,7 @@
   5.175    let
   5.176      val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
   5.177      val (iformula, atomic_Ts) =
   5.178 -      iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
   5.179 -                         []
   5.180 +      iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
   5.181        |>> close_universally add_iterm_vars
   5.182    in
   5.183      {name = name, stature = stature, role = role, iformula = iformula,
   5.184 @@ -1903,7 +1902,7 @@
   5.185      end
   5.186    | extract_lambda_def _ = raise Fail "malformed lifted lambda"
   5.187  
   5.188 -fun trans_lams_from_string ctxt type_enc lam_trans =
   5.189 +fun trans_lams_of_string ctxt type_enc lam_trans =
   5.190    if lam_trans = no_lamsN then
   5.191      rpair []
   5.192    else if lam_trans = hide_lamsN then
   5.193 @@ -1955,7 +1954,7 @@
   5.194                         concl_t facts =
   5.195    let
   5.196      val thy = Proof_Context.theory_of ctxt
   5.197 -    val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
   5.198 +    val trans_lams = trans_lams_of_string ctxt type_enc lam_trans
   5.199      val fact_ts = facts |> map snd
   5.200      (* Remove existing facts from the conjecture, as this can dramatically
   5.201         boost an ATP's performance (for some reason). *)
   5.202 @@ -2058,17 +2057,17 @@
   5.203  fun do_bound_type ctxt mono type_enc =
   5.204    case type_enc of
   5.205      Native (_, _, level) =>
   5.206 -    fused_type ctxt mono level 0 #> native_ho_type_from_typ type_enc false 0
   5.207 +    fused_type ctxt mono level 0 #> native_ho_type_of_typ type_enc false 0
   5.208      #> SOME
   5.209    | _ => K NONE
   5.210  
   5.211  fun tag_with_type ctxt mono type_enc pos T tm =
   5.212    IConst (type_tag, T --> T, [T])
   5.213    |> mangle_type_args_in_iterm type_enc
   5.214 -  |> ho_term_from_iterm ctxt mono type_enc pos
   5.215 +  |> ho_term_of_iterm ctxt mono type_enc pos
   5.216    |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
   5.217         | _ => raise Fail "unexpected lambda-abstraction")
   5.218 -and ho_term_from_iterm ctxt mono type_enc pos =
   5.219 +and ho_term_of_iterm ctxt mono type_enc pos =
   5.220    let
   5.221      fun term site u =
   5.222        let
   5.223 @@ -2094,7 +2093,7 @@
   5.224              map (term Elsewhere) args |> mk_aterm type_enc name []
   5.225            | IAbs ((name, T), tm) =>
   5.226              if is_type_enc_higher_order type_enc then
   5.227 -              AAbs (((name, native_ho_type_from_typ type_enc true 0 T), (* FIXME? why "true"? *)
   5.228 +              AAbs (((name, native_ho_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
   5.229                       term Elsewhere tm), map (term Elsewhere) args)
   5.230              else
   5.231                raise Fail "unexpected lambda-abstraction"
   5.232 @@ -2102,11 +2101,11 @@
   5.233          val tag = should_tag_with_type ctxt mono type_enc site u T
   5.234        in t |> tag ? tag_with_type ctxt mono type_enc pos T end
   5.235    in term (Top_Level pos) end
   5.236 -and formula_from_iformula ctxt mono type_enc should_guard_var =
   5.237 +and formula_of_iformula ctxt mono type_enc should_guard_var =
   5.238    let
   5.239      val thy = Proof_Context.theory_of ctxt
   5.240      val level = level_of_type_enc type_enc
   5.241 -    val do_term = ho_term_from_iterm ctxt mono type_enc
   5.242 +    val do_term = ho_term_of_iterm ctxt mono type_enc
   5.243      fun do_out_of_bound_type pos phi universal (name, T) =
   5.244        if should_guard_type ctxt mono type_enc
   5.245               (fn () => should_guard_var thy level pos phi universal name) T then
   5.246 @@ -2121,7 +2120,7 @@
   5.247        else
   5.248          NONE
   5.249      fun do_formula pos (ATyQuant (q, xs, phi)) =
   5.250 -        ATyQuant (q, map (apfst (native_ho_type_from_typ type_enc false 0)) xs,
   5.251 +        ATyQuant (q, map (apfst (native_ho_type_of_typ type_enc false 0)) xs,
   5.252                    do_formula pos phi)
   5.253        | do_formula pos (AQuant (q, xs, phi)) =
   5.254          let
   5.255 @@ -2161,7 +2160,7 @@
   5.256              encode name, alt name),
   5.257             role,
   5.258             iformula
   5.259 -           |> formula_from_iformula ctxt mono type_enc
   5.260 +           |> formula_of_iformula ctxt mono type_enc
   5.261                    should_guard_var_in_formula (if pos then SOME true else NONE)
   5.262             |> close_formula_universally
   5.263             |> bound_tvars type_enc true atomic_types,
   5.264 @@ -2188,7 +2187,7 @@
   5.265                  map (fn (cls, T) =>
   5.266                          (T |> dest_TVar |> tvar_name, map (`make_class) cls))
   5.267                      prems,
   5.268 -                native_ho_type_from_typ type_enc false 0 T, `make_class cl)
   5.269 +                native_ho_type_of_typ type_enc false 0 T, `make_class cl)
   5.270    else
   5.271      Formula ((tcon_clause_prefix ^ name, ""), Axiom,
   5.272               mk_ahorn (maps (class_atoms type_enc) prems)
   5.273 @@ -2200,7 +2199,7 @@
   5.274                         ({name, role, iformula, atomic_types, ...} : ifact) =
   5.275    Formula ((conjecture_prefix ^ name, ""), role,
   5.276             iformula
   5.277 -           |> formula_from_iformula ctxt mono type_enc
   5.278 +           |> formula_of_iformula ctxt mono type_enc
   5.279                    should_guard_var_in_formula (SOME false)
   5.280             |> close_formula_universally
   5.281             |> bound_tvars type_enc true atomic_types, NONE, [])
   5.282 @@ -2213,8 +2212,7 @@
   5.283        fun line j (cl, T) =
   5.284          if type_classes then
   5.285            Class_Memb (class_memb_prefix ^ string_of_int j, [],
   5.286 -                      native_ho_type_from_typ type_enc false 0 T,
   5.287 -                      `make_class cl)
   5.288 +                      native_ho_type_of_typ type_enc false 0 T, `make_class cl)
   5.289          else
   5.290            Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
   5.291                     class_atom type_enc (cl, T), NONE, [])
   5.292 @@ -2386,8 +2384,8 @@
   5.293             IConst (`make_bound_var "X", T, [])
   5.294             |> type_guard_iterm type_enc T
   5.295             |> AAtom
   5.296 -           |> formula_from_iformula ctxt mono type_enc
   5.297 -                                    always_guard_var_in_formula (SOME true)
   5.298 +           |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula
   5.299 +                                  (SOME true)
   5.300             |> close_formula_universally
   5.301             |> bound_tvars type_enc true (atomic_types_of T),
   5.302             NONE, isabelle_info inductiveN helper_rank)
   5.303 @@ -2423,7 +2421,7 @@
   5.304    in
   5.305      Sym_Decl (sym_decl_prefix ^ s, (s, s'),
   5.306                T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
   5.307 -                |> native_ho_type_from_typ type_enc pred_sym ary
   5.308 +                |> native_ho_type_of_typ type_enc pred_sym ary
   5.309                  |> not (null T_args)
   5.310                     ? curry APi (map (tvar_name o dest_TVar) T_args))
   5.311    end
   5.312 @@ -2456,8 +2454,8 @@
   5.313               |> fold (curry (IApp o swap)) bounds
   5.314               |> type_guard_iterm type_enc res_T
   5.315               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
   5.316 -             |> formula_from_iformula ctxt mono type_enc
   5.317 -                                      always_guard_var_in_formula (SOME true)
   5.318 +             |> formula_of_iformula ctxt mono type_enc
   5.319 +                                    always_guard_var_in_formula (SOME true)
   5.320               |> close_formula_universally
   5.321               |> bound_tvars type_enc (n > 1) (atomic_types_of T)
   5.322               |> maybe_negate,
   5.323 @@ -2544,15 +2542,15 @@
   5.324                             (type_enc as Native (_, _, level)) sym_tab =
   5.325      let
   5.326        val thy = Proof_Context.theory_of ctxt
   5.327 -      val ho_term_from_term =
   5.328 -        iterm_from_term thy type_enc []
   5.329 -        #> fst #> ho_term_from_iterm ctxt mono type_enc NONE
   5.330 +      val ho_term_of_term =
   5.331 +        iterm_of_term thy type_enc []
   5.332 +        #> fst #> ho_term_of_iterm ctxt mono type_enc NONE
   5.333      in
   5.334        if is_type_enc_polymorphic type_enc then
   5.335 -        [(native_ho_type_from_typ type_enc false 0 @{typ nat},
   5.336 -          map ho_term_from_term [@{term "0::nat"}, @{term Suc}], true) (*,
   5.337 -         (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
   5.338 -          map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
   5.339 +        [(native_ho_type_of_typ type_enc false 0 @{typ nat},
   5.340 +          map ho_term_of_term [@{term "0::nat"}, @{term Suc}], true) (*,
   5.341 +         (native_ho_type_of_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
   5.342 +          map (ho_term_of_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
   5.343            true) *)]
   5.344        else
   5.345          []
   5.346 @@ -2584,7 +2582,7 @@
   5.347          val base_ary = min_ary_of sym_tab0 base_s
   5.348          fun do_const name = IConst (name, T, T_args)
   5.349          val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc
   5.350 -        val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
   5.351 +        val ho_term_of = ho_term_of_iterm ctxt mono type_enc (SOME true)
   5.352          val name1 as (s1, _) =
   5.353            base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
   5.354          val name2 as (s2, _) = base_name |> aliased_uncurried ary
     6.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu May 16 13:19:27 2013 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu May 16 13:34:13 2013 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4    val parse_formula :
     6.5      string list
     6.6      -> (string, 'a, (string, 'a) ho_term, string) formula * string list
     6.7 -  val atp_proof_from_tstplike_proof : string problem -> string -> string proof
     6.8 +  val atp_proof_of_tstplike_proof : string problem -> string -> string proof
     6.9    val clean_up_atp_proof_dependencies : string proof -> string proof
    6.10    val map_term_names_in_atp_proof :
    6.11      (string -> string) -> string proof -> string proof
    6.12 @@ -493,8 +493,8 @@
    6.13                           (Scan.repeat1 (parse_line problem))))
    6.14    #> fst
    6.15  
    6.16 -fun atp_proof_from_tstplike_proof _ "" = []
    6.17 -  | atp_proof_from_tstplike_proof problem tstp =
    6.18 +fun atp_proof_of_tstplike_proof _ "" = []
    6.19 +  | atp_proof_of_tstplike_proof problem tstp =
    6.20      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    6.21      |> parse_proof problem
    6.22      |> sort (step_name_ord o pairself #1)
     7.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
     7.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
     7.3 @@ -26,10 +26,10 @@
     7.4    val forall_of : term -> term -> term
     7.5    val exists_of : term -> term -> term
     7.6    val unalias_type_enc : string -> string list
     7.7 -  val term_from_atp :
     7.8 +  val term_of_atp :
     7.9      Proof.context -> bool -> int Symtab.table -> typ option ->
    7.10      (string, string) ho_term -> term
    7.11 -  val prop_from_atp :
    7.12 +  val prop_of_atp :
    7.13      Proof.context -> bool -> int Symtab.table ->
    7.14      (string, string, (string, string) ho_term, string) formula -> term
    7.15  end;
    7.16 @@ -97,8 +97,8 @@
    7.17  
    7.18  (* Type variables are given the basic sort "HOL.type". Some will later be
    7.19     constrained by information from type literals, or by type inference. *)
    7.20 -fun typ_from_atp ctxt (u as ATerm ((a, _), us)) =
    7.21 -  let val Ts = map (typ_from_atp ctxt) us in
    7.22 +fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =
    7.23 +  let val Ts = map (typ_of_atp ctxt) us in
    7.24      case unprefix_and_unascii type_const_prefix a of
    7.25        SOME b => Type (invert_const b, Ts)
    7.26      | NONE =>
    7.27 @@ -117,8 +117,8 @@
    7.28  
    7.29  (* Type class literal applied to a type. Returns triple of polarity, class,
    7.30     type. *)
    7.31 -fun type_constraint_from_term ctxt (u as ATerm ((a, _), us)) =
    7.32 -  case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
    7.33 +fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) =
    7.34 +  case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of
    7.35      (SOME b, [T]) => (b, T)
    7.36    | _ => raise HO_TERM [u]
    7.37  
    7.38 @@ -166,7 +166,7 @@
    7.39  
    7.40  (* First-order translation. No types are known for variables. "HOLogic.typeT"
    7.41     should allow them to be inferred. *)
    7.42 -fun term_from_atp ctxt textual sym_tab =
    7.43 +fun term_of_atp ctxt textual sym_tab =
    7.44    let
    7.45      val thy = Proof_Context.theory_of ctxt
    7.46      (* For Metis, we use 1 rather than 0 because variable references in clauses
    7.47 @@ -198,7 +198,7 @@
    7.48              if s' = type_tag_name then
    7.49                case mangled_us @ us of
    7.50                  [typ_u, term_u] =>
    7.51 -                do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
    7.52 +                do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u
    7.53                | _ => raise HO_TERM us
    7.54              else if s' = predicator_name then
    7.55                do_term [] (SOME @{typ bool}) (hd us)
    7.56 @@ -223,7 +223,7 @@
    7.57                  val T =
    7.58                    (if not (null type_us) andalso
    7.59                        num_type_args thy s' = length type_us then
    7.60 -                     let val Ts = type_us |> map (typ_from_atp ctxt) in
    7.61 +                     let val Ts = type_us |> map (typ_of_atp ctxt) in
    7.62                         if new_skolem then
    7.63                           SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
    7.64                         else if textual then
    7.65 @@ -240,7 +240,7 @@
    7.66                                    | NONE => HOLogic.typeT))
    7.67                  val t =
    7.68                    if new_skolem then
    7.69 -                    Var ((new_skolem_var_name_from_const s'', var_index), T)
    7.70 +                    Var ((new_skolem_var_name_of_const s'', var_index), T)
    7.71                    else
    7.72                      Const (unproxify_const s', T)
    7.73                in list_comb (t, term_ts @ extra_ts) end
    7.74 @@ -277,12 +277,12 @@
    7.75            in list_comb (t, ts) end
    7.76    in do_term [] end
    7.77  
    7.78 -fun term_from_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
    7.79 +fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
    7.80    if String.isPrefix class_prefix s then
    7.81 -    add_type_constraint pos (type_constraint_from_term ctxt u)
    7.82 +    add_type_constraint pos (type_constraint_of_term ctxt u)
    7.83      #> pair @{const True}
    7.84    else
    7.85 -    pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
    7.86 +    pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
    7.87  
    7.88  (* Update schematic type variables with detected sort constraints. It's not
    7.89     totally clear whether this code is necessary. *)
    7.90 @@ -308,7 +308,7 @@
    7.91  
    7.92  (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    7.93     appear in the formula. *)
    7.94 -fun prop_from_atp ctxt textual sym_tab phi =
    7.95 +fun prop_of_atp ctxt textual sym_tab phi =
    7.96    let
    7.97      fun do_formula pos phi =
    7.98        case phi of
    7.99 @@ -329,7 +329,7 @@
   7.100               | AImplies => s_imp
   7.101               | AIff => s_iff
   7.102               | ANot => raise Fail "impossible connective")
   7.103 -      | AAtom tm => term_from_atom ctxt textual sym_tab pos tm
   7.104 +      | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
   7.105        | _ => raise FORMULA [phi]
   7.106    in repair_tvar_sorts (do_formula true phi Vartab.empty) end
   7.107  
     8.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Thu May 16 13:19:27 2013 +0200
     8.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Thu May 16 13:34:13 2013 +0200
     8.3 @@ -17,8 +17,8 @@
     8.4    val nat_subscript : int -> string
     8.5    val unyxml : string -> string
     8.6    val maybe_quote : string -> string
     8.7 -  val string_from_ext_time : bool * Time.time -> string
     8.8 -  val string_from_time : Time.time -> string
     8.9 +  val string_of_ext_time : bool * Time.time -> string
    8.10 +  val string_of_time : Time.time -> string
    8.11    val type_instance : theory -> typ -> typ -> bool
    8.12    val type_generalization : theory -> typ -> typ -> bool
    8.13    val type_intersect : theory -> typ -> typ -> bool
    8.14 @@ -134,7 +134,7 @@
    8.15             Keyword.is_keyword s) ? quote
    8.16    end
    8.17  
    8.18 -fun string_from_ext_time (plus, time) =
    8.19 +fun string_of_ext_time (plus, time) =
    8.20    let val ms = Time.toMilliseconds time in
    8.21      (if plus then "> " else "") ^
    8.22      (if plus andalso ms mod 1000 = 0 then
    8.23 @@ -145,7 +145,7 @@
    8.24         string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
    8.25    end
    8.26  
    8.27 -val string_from_time = string_from_ext_time o pair false
    8.28 +val string_of_time = string_of_ext_time o pair false
    8.29  
    8.30  fun type_instance thy T T' = Sign.typ_instance thy (T, T')
    8.31  fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
     9.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 16 13:19:27 2013 +0200
     9.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 16 13:34:13 2013 +0200
     9.3 @@ -191,7 +191,7 @@
     9.4  (* Given the definition of a Skolem function, return a theorem to replace
     9.5     an existential formula by a use of that function.
     9.6     Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
     9.7 -fun old_skolem_theorem_from_def thy rhs0 =
     9.8 +fun old_skolem_theorem_of_def thy rhs0 =
     9.9    let
    9.10      val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
    9.11      val rhs' = rhs |> Thm.dest_comb |> snd
    9.12 @@ -200,7 +200,7 @@
    9.13      val T =
    9.14        case hilbert of
    9.15          Const (_, Type (@{type_name fun}, [_, T])) => T
    9.16 -      | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
    9.17 +      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
    9.18                           [hilbert])
    9.19      val cex = cterm_of thy (HOLogic.exists_const T)
    9.20      val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
    9.21 @@ -372,7 +372,7 @@
    9.22        nnf_axiom choice_ths new_skolem ax_no th ctxt0
    9.23      fun clausify th =
    9.24        make_cnf (if new_skolem orelse null choice_ths then []
    9.25 -                else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
    9.26 +                else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
    9.27                 th ctxt ctxt
    9.28      val (cnf_ths, ctxt) = clausify nnf_th
    9.29      fun intr_imp ct th =
    10.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Thu May 16 13:19:27 2013 +0200
    10.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu May 16 13:34:13 2013 +0200
    10.3 @@ -138,7 +138,7 @@
    10.4  val prepare_helper =
    10.5    Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
    10.6  
    10.7 -fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
    10.8 +fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
    10.9    if is_tptp_variable s then
   10.10      Metis_Term.Var (Metis_Name.fromString s)
   10.11    else
   10.12 @@ -147,24 +147,23 @@
   10.13       | NONE => (s, false))
   10.14      |> (fn (s, swap) =>
   10.15             Metis_Term.Fn (Metis_Name.fromString s,
   10.16 -                          tms |> map (metis_term_from_atp type_enc)
   10.17 +                          tms |> map (metis_term_of_atp type_enc)
   10.18                                |> swap ? rev))
   10.19 -fun metis_atom_from_atp type_enc (AAtom tm) =
   10.20 -    (case metis_term_from_atp type_enc tm of
   10.21 +fun metis_atom_of_atp type_enc (AAtom tm) =
   10.22 +    (case metis_term_of_atp type_enc tm of
   10.23         Metis_Term.Fn x => x
   10.24       | _ => raise Fail "non CNF -- expected function")
   10.25 -  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
   10.26 -fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
   10.27 -    (false, metis_atom_from_atp type_enc phi)
   10.28 -  | metis_literal_from_atp type_enc phi =
   10.29 -    (true, metis_atom_from_atp type_enc phi)
   10.30 -fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
   10.31 -    maps (metis_literals_from_atp type_enc) phis
   10.32 -  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
   10.33 -fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
   10.34 +  | metis_atom_of_atp _ _ = raise Fail "not CNF -- expected atom"
   10.35 +fun metis_literal_of_atp type_enc (AConn (ANot, [phi])) =
   10.36 +    (false, metis_atom_of_atp type_enc phi)
   10.37 +  | metis_literal_of_atp type_enc phi = (true, metis_atom_of_atp type_enc phi)
   10.38 +fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
   10.39 +    maps (metis_literals_of_atp type_enc) phis
   10.40 +  | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
   10.41 +fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
   10.42      let
   10.43        fun some isa =
   10.44 -        SOME (phi |> metis_literals_from_atp type_enc
   10.45 +        SOME (phi |> metis_literals_of_atp type_enc
   10.46                    |> Metis_LiteralSet.fromList
   10.47                    |> Metis_Thm.axiom, isa)
   10.48      in
   10.49 @@ -197,7 +196,7 @@
   10.50          end
   10.51        | NONE => TrueI |> Isa_Raw |> some
   10.52      end
   10.53 -  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
   10.54 +  | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
   10.55  
   10.56  fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
   10.57      eliminate_lam_wrappers t
   10.58 @@ -251,7 +250,7 @@
   10.59      (* "rev" is for compatibility with existing proof scripts. *)
   10.60      val axioms =
   10.61        atp_problem
   10.62 -      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
   10.63 +      |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
   10.64      fun ord_info () = atp_problem_term_order_info atp_problem
   10.65    in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
   10.66  
    11.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
    11.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
    11.3 @@ -13,7 +13,7 @@
    11.4  
    11.5    exception METIS_RECONSTRUCT of string * string
    11.6  
    11.7 -  val hol_clause_from_metis :
    11.8 +  val hol_clause_of_metis :
    11.9      Proof.context -> type_enc -> int Symtab.table
   11.10      -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
   11.11    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
   11.12 @@ -36,40 +36,40 @@
   11.13  
   11.14  exception METIS_RECONSTRUCT of string * string
   11.15  
   11.16 -fun atp_name_from_metis type_enc s =
   11.17 +fun atp_name_of_metis type_enc s =
   11.18    case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
   11.19      SOME ((s, _), (_, swap)) => (s, swap)
   11.20    | _ => (s, false)
   11.21 -fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
   11.22 -    let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
   11.23 -      ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
   11.24 +fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
   11.25 +    let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
   11.26 +      ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
   11.27      end
   11.28 -  | atp_term_from_metis _ (Metis_Term.Var s) =
   11.29 +  | atp_term_of_metis _ (Metis_Term.Var s) =
   11.30      ATerm ((Metis_Name.toString s, []), [])
   11.31  
   11.32 -fun hol_term_from_metis ctxt type_enc sym_tab =
   11.33 -  atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
   11.34 +fun hol_term_of_metis ctxt type_enc sym_tab =
   11.35 +  atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
   11.36  
   11.37 -fun atp_literal_from_metis type_enc (pos, atom) =
   11.38 -  atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
   11.39 +fun atp_literal_of_metis type_enc (pos, atom) =
   11.40 +  atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
   11.41         |> AAtom |> not pos ? mk_anot
   11.42 -fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
   11.43 -  | atp_clause_from_metis type_enc lits =
   11.44 -    lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
   11.45 +fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
   11.46 +  | atp_clause_of_metis type_enc lits =
   11.47 +    lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
   11.48  
   11.49  fun polish_hol_terms ctxt (lifted, old_skolems) =
   11.50    map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
   11.51    #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
   11.52  
   11.53 -fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
   11.54 +fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
   11.55    Metis_Thm.clause
   11.56    #> Metis_LiteralSet.toList
   11.57 -  #> atp_clause_from_metis type_enc
   11.58 -  #> prop_from_atp ctxt false sym_tab
   11.59 +  #> atp_clause_of_metis type_enc
   11.60 +  #> prop_of_atp ctxt false sym_tab
   11.61    #> singleton (polish_hol_terms ctxt concealed)
   11.62  
   11.63 -fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
   11.64 -  let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
   11.65 +fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
   11.66 +  let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
   11.67        val _ = trace_msg ctxt (fn () => "  calling type inference:")
   11.68        val _ = app (fn t => trace_msg ctxt
   11.69                                       (fn () => Syntax.string_of_term ctxt t)) ts
   11.70 @@ -102,7 +102,7 @@
   11.71  (* INFERENCE RULE: AXIOM *)
   11.72  
   11.73  (* This causes variables to have an index of 1 by default. See also
   11.74 -   "term_from_atp" in "ATP_Proof_Reconstruct". *)
   11.75 +   "term_of_atp" in "ATP_Proof_Reconstruct". *)
   11.76  val axiom_inference = Thm.incr_indexes 1 oo lookth
   11.77  
   11.78  (* INFERENCE RULE: ASSUME *)
   11.79 @@ -118,7 +118,7 @@
   11.80  fun assume_inference ctxt type_enc concealed sym_tab atom =
   11.81    inst_excluded_middle
   11.82        (Proof_Context.theory_of ctxt)
   11.83 -      (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
   11.84 +      (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
   11.85                   (Metis_Term.Fn atom))
   11.86  
   11.87  (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
   11.88 @@ -134,14 +134,14 @@
   11.89        fun subst_translation (x,y) =
   11.90          let val v = find_var x
   11.91              (* We call "polish_hol_terms" below. *)
   11.92 -            val t = hol_term_from_metis ctxt type_enc sym_tab y
   11.93 +            val t = hol_term_of_metis ctxt type_enc sym_tab y
   11.94          in  SOME (cterm_of thy (Var v), t)  end
   11.95          handle Option.Option =>
   11.96                 (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   11.97                                           " in " ^ Display.string_of_thm ctxt i_th);
   11.98                  NONE)
   11.99               | TYPE _ =>
  11.100 -               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
  11.101 +               (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^
  11.102                                           " in " ^ Display.string_of_thm ctxt i_th);
  11.103                  NONE)
  11.104        fun remove_typeinst (a, t) =
  11.105 @@ -275,7 +275,7 @@
  11.106        let
  11.107          val thy = Proof_Context.theory_of ctxt
  11.108          val i_atom =
  11.109 -          singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
  11.110 +          singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
  11.111                      (Metis_Term.Fn atom)
  11.112          val _ = trace_msg ctxt (fn () =>
  11.113                      "  atom: " ^ Syntax.string_of_term ctxt i_atom)
  11.114 @@ -309,7 +309,7 @@
  11.115    let
  11.116      val thy = Proof_Context.theory_of ctxt
  11.117      val i_t =
  11.118 -      singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
  11.119 +      singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
  11.120      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
  11.121      val c_t = cterm_incr_types thy refl_idx i_t
  11.122    in cterm_instantiate [(refl_x, c_t)] REFL_THM end
  11.123 @@ -323,7 +323,7 @@
  11.124    let val thy = Proof_Context.theory_of ctxt
  11.125        val m_tm = Metis_Term.Fn atom
  11.126        val [i_atom, i_tm] =
  11.127 -        hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
  11.128 +        hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
  11.129        val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
  11.130        fun replace_item_list lx 0 (_::ls) = lx::ls
  11.131          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
    12.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu May 16 13:19:27 2013 +0200
    12.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu May 16 13:34:13 2013 +0200
    12.3 @@ -47,9 +47,9 @@
    12.4     "t => t'", where "t" and "t'" are the same term modulo type tags.
    12.5     In Isabelle, type tags are stripped away, so we are left with "t = t" or
    12.6     "t => t". Type tag idempotence is also handled this way. *)
    12.7 -fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
    12.8 +fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
    12.9    let val thy = Proof_Context.theory_of ctxt in
   12.10 -    case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
   12.11 +    case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
   12.12        Const (@{const_name HOL.eq}, _) $ _ $ t =>
   12.13        let
   12.14          val ct = cterm_of thy t
   12.15 @@ -62,11 +62,11 @@
   12.16    end
   12.17    |> Meson.make_meta_clause
   12.18  
   12.19 -fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
   12.20 +fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
   12.21    let
   12.22      val thy = Proof_Context.theory_of ctxt
   12.23      val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
   12.24 -    val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
   12.25 +    val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
   12.26      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
   12.27    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
   12.28  
   12.29 @@ -158,13 +158,13 @@
   12.30        val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
   12.31        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
   12.32        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
   12.33 -      val type_enc = type_enc_from_string Strict type_enc
   12.34 +      val type_enc = type_enc_of_string Strict type_enc
   12.35        val (sym_tab, axioms, ord_info, concealed) =
   12.36          prepare_metis_problem ctxt type_enc lam_trans cls ths
   12.37        fun get_isa_thm mth Isa_Reflexive_or_Trivial =
   12.38 -          reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
   12.39 +          reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
   12.40          | get_isa_thm mth Isa_Lambda_Lifted =
   12.41 -          lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
   12.42 +          lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
   12.43          | get_isa_thm _ (Isa_Raw ith) = ith
   12.44        val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
   12.45        val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
    13.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:19:27 2013 +0200
    13.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:34:13 2013 +0200
    13.3 @@ -1051,7 +1051,7 @@
    13.4               (print_nt (fn () => excipit "ran out of time after checking");
    13.5                if !met_potential > 0 then potentialN else unknownN)
    13.6      val _ = print_v (fn () =>
    13.7 -                "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
    13.8 +                "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
    13.9                  ".")
   13.10    in (outcome_code, !state_ref) end
   13.11  
    14.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu May 16 13:19:27 2013 +0200
    14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu May 16 13:34:13 2013 +0200
    14.3 @@ -52,7 +52,7 @@
    14.4    val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
    14.5    val parse_bool_option : bool -> string -> string -> bool option
    14.6    val parse_time_option : string -> string -> Time.time option
    14.7 -  val string_from_time : Time.time -> string
    14.8 +  val string_of_time : Time.time -> string
    14.9    val nat_subscript : int -> string
   14.10    val flip_polarity : polarity -> polarity
   14.11    val prop_T : typ
   14.12 @@ -237,7 +237,7 @@
   14.13  
   14.14  val parse_bool_option = Sledgehammer_Util.parse_bool_option
   14.15  val parse_time_option = Sledgehammer_Util.parse_time_option
   14.16 -val string_from_time = ATP_Util.string_from_time
   14.17 +val string_of_time = ATP_Util.string_of_time
   14.18  
   14.19  val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
   14.20  fun nat_subscript n =
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:19:27 2013 +0200
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:34:13 2013 +0200
    15.3 @@ -21,7 +21,7 @@
    15.4    val ignore_no_atp : bool Config.T
    15.5    val instantiate_inducts : bool Config.T
    15.6    val no_fact_override : fact_override
    15.7 -  val fact_from_ref :
    15.8 +  val fact_of_ref :
    15.9      Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
   15.10      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   15.11    val backquote_thm : Proof.context -> thm -> string
   15.12 @@ -119,7 +119,7 @@
   15.13  fun stature_of_thm global assms chained css name th =
   15.14    (scope_of_thm global assms chained th, status_of_thm css name th)
   15.15  
   15.16 -fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
   15.17 +fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   15.18    let
   15.19      val ths = Attrib.eval_thms ctxt [xthm]
   15.20      val bracket =
   15.21 @@ -502,7 +502,7 @@
   15.22      in
   15.23        (if only then
   15.24           maps (map (fn ((name, stature), th) => ((K name, stature), th))
   15.25 -               o fact_from_ref ctxt reserved chained css) add
   15.26 +               o fact_of_ref ctxt reserved chained css) add
   15.27         else
   15.28           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
   15.29             all_facts ctxt false ho_atp reserved add chained css
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 16 13:19:27 2013 +0200
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 16 13:34:13 2013 +0200
    16.3 @@ -159,7 +159,7 @@
    16.4                              | _ => value)
    16.5      | NONE => (name, value)
    16.6  
    16.7 -val any_type_enc = type_enc_from_string Strict "erased"
    16.8 +val any_type_enc = type_enc_of_string Strict "erased"
    16.9  
   16.10  (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
   16.11     can be omitted. For the last four, this is a secret feature. *)
   16.12 @@ -171,9 +171,9 @@
   16.13           else if null value then
   16.14             if is_prover_list ctxt name then
   16.15               ("provers", [name])
   16.16 -           else if can (type_enc_from_string Strict) name then
   16.17 +           else if can (type_enc_of_string Strict) name then
   16.18               ("type_enc", [name])
   16.19 -           else if can (trans_lams_from_string ctxt any_type_enc) name then
   16.20 +           else if can (trans_lams_of_string ctxt any_type_enc) name then
   16.21               ("lam_trans", [name])
   16.22             else if member (op =) fact_filters name then
   16.23               ("fact_filter", [name])
   16.24 @@ -295,7 +295,7 @@
   16.25          NONE
   16.26        else case lookup_string "type_enc" of
   16.27          "smart" => NONE
   16.28 -      | s => (type_enc_from_string Strict s; SOME s)
   16.29 +      | s => (type_enc_of_string Strict s; SOME s)
   16.30      val strict = mode = Auto_Try orelse lookup_bool "strict"
   16.31      val lam_trans = lookup_option lookup_string "lam_trans"
   16.32      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 16 13:19:27 2013 +0200
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 16 13:34:13 2013 +0200
    17.3 @@ -1024,7 +1024,7 @@
    17.4                 "Learned " ^ string_of_int num_proofs ^ " " ^
    17.5                 (if run_prover then "automatic" else "Isar") ^ " proof" ^
    17.6                 plural_s num_proofs ^ " in the last " ^
    17.7 -               string_from_time commit_timeout ^ "."
    17.8 +               string_of_time commit_timeout ^ "."
    17.9                 |> Output.urgent_message
   17.10               end
   17.11             else
   17.12 @@ -1111,10 +1111,8 @@
   17.13          if verbose orelse auto_level < 2 then
   17.14            "Learned " ^ string_of_int n ^ " nontrivial " ^
   17.15            (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
   17.16 -          (if verbose then
   17.17 -             " in " ^ string_from_time (Timer.checkRealTimer timer)
   17.18 -           else
   17.19 -             "") ^ "."
   17.20 +          (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
   17.21 +           else "") ^ "."
   17.22          else
   17.23            ""
   17.24        end
   17.25 @@ -1138,7 +1136,7 @@
   17.26        ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
   17.27         plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
   17.28         (case timeout of
   17.29 -          SOME timeout => " timeout: " ^ string_from_time timeout
   17.30 +          SOME timeout => " timeout: " ^ string_of_time timeout
   17.31          | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
   17.32         |> Output.urgent_message;
   17.33         learn 1 false;
    18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 16 13:19:27 2013 +0200
    18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 16 13:34:13 2013 +0200
    18.3 @@ -65,7 +65,7 @@
    18.4            "Testing " ^ n_facts (map fst facts) ^
    18.5            (if verbose then
    18.6               case timeout of
    18.7 -               SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
    18.8 +               SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")"
    18.9               | _ => ""
   18.10             else
   18.11               "") ^ "...")
   18.12 @@ -96,7 +96,7 @@
   18.13                  "Found proof" ^
   18.14                   (if length used_facts = length facts then ""
   18.15                    else " with " ^ n_facts used_facts) ^
   18.16 -                 " (" ^ string_from_time run_time ^ ").");
   18.17 +                 " (" ^ string_of_time run_time ^ ").");
   18.18      result
   18.19    end
   18.20  
   18.21 @@ -351,7 +351,7 @@
   18.22      val css = clasimpset_rule_table_of ctxt
   18.23      val facts =
   18.24        refs |> maps (map (apsnd single)
   18.25 -                    o fact_from_ref ctxt reserved chained_ths css)
   18.26 +                    o fact_of_ref ctxt reserved chained_ths css)
   18.27    in
   18.28      case subgoal_count state of
   18.29        0 => Output.urgent_message "No subgoal!"
    19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu May 16 13:19:27 2013 +0200
    19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu May 16 13:34:13 2013 +0200
    19.3 @@ -36,7 +36,7 @@
    19.4  
    19.5  fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
    19.6  
    19.7 -val string_of_preplay_time = ATP_Util.string_from_ext_time
    19.8 +val string_of_preplay_time = ATP_Util.string_of_ext_time
    19.9  
   19.10  (* preplay tracing *)
   19.11  fun preplay_trace ctxt assms concl time =
    20.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 13:19:27 2013 +0200
    20.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 13:34:13 2013 +0200
    20.3 @@ -530,7 +530,7 @@
    20.4                  if verbose then
    20.5                    "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
    20.6                    (case timeout of
    20.7 -                     SOME timeout => " for " ^ string_from_time timeout
    20.8 +                     SOME timeout => " for " ^ string_of_time timeout
    20.9                     | NONE => "") ^ "..."
   20.10                    |> Output.urgent_message
   20.11                  else
   20.12 @@ -616,7 +616,7 @@
   20.13  
   20.14  fun choose_type_enc soundness best_type_enc format =
   20.15    the_default best_type_enc
   20.16 -  #> type_enc_from_string soundness
   20.17 +  #> type_enc_of_string soundness
   20.18    #> adjust_type_enc format
   20.19  
   20.20  fun isar_proof_reconstructor ctxt name =
   20.21 @@ -793,7 +793,7 @@
   20.22                  " with " ^ string_of_int num_facts ^ " fact" ^
   20.23                  plural_s num_facts ^
   20.24                  (case slice_timeout of
   20.25 -                   SOME timeout => " for " ^ string_from_time timeout
   20.26 +                   SOME timeout => " for " ^ string_of_time timeout
   20.27                   | NONE => "") ^ "..."
   20.28                  |> Output.urgent_message
   20.29                else
   20.30 @@ -849,7 +849,7 @@
   20.31                       (accum, facts,
   20.32                        extract_tstplike_proof_and_outcome verbose proof_delims
   20.33                                                           known_failures output
   20.34 -                      |>> atp_proof_from_tstplike_proof atp_problem
   20.35 +                      |>> atp_proof_of_tstplike_proof atp_problem
   20.36                        handle UNRECOGNIZED_ATP_PROOF () =>
   20.37                               ([], SOME ProofIncomplete)))
   20.38                handle TimeLimit.TimeOut =>
   20.39 @@ -921,7 +921,7 @@
   20.40            val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
   20.41            val reconstrs =
   20.42              bunch_of_reconstructors needs_full_types
   20.43 -                (lam_trans_from_atp_proof atp_proof
   20.44 +                (lam_trans_of_atp_proof atp_proof
   20.45                   o (fn desperate => if desperate then hide_lamsN
   20.46                                      else metis_default_lam_trans))
   20.47          in
   20.48 @@ -955,7 +955,7 @@
   20.49                             one_line_params
   20.50                end,
   20.51             (if verbose then
   20.52 -              "\nATP real CPU time: " ^ string_from_time run_time ^ "."
   20.53 +              "\nATP real CPU time: " ^ string_of_time run_time ^ "."
   20.54              else
   20.55                "") ^
   20.56             (if important_message <> "" then
   20.57 @@ -991,17 +991,16 @@
   20.58     (139, Crashed)]
   20.59  val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
   20.60  
   20.61 -fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
   20.62 +fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
   20.63      if is_real_cex then Unprovable else GaveUp
   20.64 -  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   20.65 -  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
   20.66 +  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
   20.67 +  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
   20.68      (case AList.lookup (op =) smt_failures code of
   20.69         SOME failure => failure
   20.70       | NONE => UnknownError ("Abnormal termination with exit code " ^
   20.71                               string_of_int code ^ "."))
   20.72 -  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   20.73 -  | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
   20.74 -    UnknownError msg
   20.75 +  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
   20.76 +  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
   20.77  
   20.78  (* FUDGE *)
   20.79  val smt_max_slices =
   20.80 @@ -1059,7 +1058,7 @@
   20.81              quote name ^ " slice " ^ string_of_int slice ^ " with " ^
   20.82              string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
   20.83              (case slice_timeout of
   20.84 -               SOME timeout => " for " ^ string_from_time timeout
   20.85 +               SOME timeout => " for " ^ string_of_time timeout
   20.86               | NONE => "") ^ "..."
   20.87              |> Output.urgent_message
   20.88            else
   20.89 @@ -1112,7 +1111,7 @@
   20.90                if verbose andalso is_some outcome then
   20.91                  quote name ^ " invoked with " ^
   20.92                  num_of_facts fact_filter num_facts ^ ": " ^
   20.93 -                string_of_failure (failure_from_smt_failure (the outcome)) ^
   20.94 +                string_of_failure (failure_of_smt_failure (the outcome)) ^
   20.95                  " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
   20.96                  "..."
   20.97                  |> Output.urgent_message
   20.98 @@ -1142,7 +1141,7 @@
   20.99      val {outcome, used_facts = used_pairs, used_from, run_time} =
  20.100        smt_filter_loop name params state goal subgoal weighted_factss
  20.101      val used_facts = used_pairs |> map fst
  20.102 -    val outcome = outcome |> Option.map failure_from_smt_failure
  20.103 +    val outcome = outcome |> Option.map failure_of_smt_failure
  20.104      val (preplay, message, message_tail) =
  20.105        case outcome of
  20.106          NONE =>
  20.107 @@ -1161,7 +1160,7 @@
  20.108                val num_chained = length (#facts (Proof.goal state))
  20.109              in one_line_proof_text num_chained one_line_params end,
  20.110           if verbose then
  20.111 -           "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
  20.112 +           "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
  20.113           else
  20.114             "")
  20.115        | SOME failure =>
    21.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
    21.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
    21.3 @@ -28,7 +28,7 @@
    21.4  
    21.5    val smtN : string
    21.6    val string_of_reconstructor : reconstructor -> string
    21.7 -  val lam_trans_from_atp_proof : string proof -> string -> string
    21.8 +  val lam_trans_of_atp_proof : string proof -> string -> string
    21.9    val is_typed_helper_used_in_atp_proof : string proof -> bool
   21.10    val used_facts_in_atp_proof :
   21.11      Proof.context -> (string * stature) list vector -> string proof ->
   21.12 @@ -121,7 +121,7 @@
   21.13  fun is_axiom_used_in_proof pred =
   21.14    exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
   21.15  
   21.16 -fun lam_trans_from_atp_proof atp_proof default =
   21.17 +fun lam_trans_of_atp_proof atp_proof default =
   21.18    case (is_axiom_used_in_proof is_combinator_def atp_proof,
   21.19          is_axiom_used_in_proof is_lam_lifted atp_proof) of
   21.20      (false, false) => default
   21.21 @@ -190,7 +190,7 @@
   21.22  (** one-liner reconstructor proofs **)
   21.23  
   21.24  fun show_time NONE = ""
   21.25 -  | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
   21.26 +  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
   21.27  
   21.28  (* FIXME: Various bugs, esp. with "unfolding"
   21.29  fun unusing_chained_facts _ 0 = ""
   21.30 @@ -279,12 +279,12 @@
   21.31    | label_of_clause c =
   21.32      (space_implode "___" (map (fst o raw_label_of_name) c), 0)
   21.33  
   21.34 -fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
   21.35 +fun add_fact_of_dependencies fact_names (names as [(_, ss)]) =
   21.36      if is_fact fact_names ss then
   21.37        apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
   21.38      else
   21.39        apfst (insert (op =) (label_of_clause names))
   21.40 -  | add_fact_from_dependencies fact_names names =
   21.41 +  | add_fact_of_dependencies fact_names names =
   21.42      apfst (insert (op =) (label_of_clause names))
   21.43  
   21.44  fun repair_name "$true" = "c_True"
   21.45 @@ -325,7 +325,7 @@
   21.46  fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
   21.47    let
   21.48      val thy = Proof_Context.theory_of ctxt
   21.49 -    val t = u |> prop_from_atp ctxt true sym_tab
   21.50 +    val t = u |> prop_of_atp ctxt true sym_tab
   21.51                |> uncombine_term thy |> infer_formula_types ctxt
   21.52    in
   21.53      ((name, role, t, rule, deps),
   21.54 @@ -648,7 +648,7 @@
   21.55      val type_enc =
   21.56        if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
   21.57        else partial_typesN
   21.58 -    val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
   21.59 +    val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
   21.60      val preplay = preplay_timeout <> SOME Time.zeroTime
   21.61  
   21.62      fun isar_proof_of () =
   21.63 @@ -744,7 +744,7 @@
   21.64                    val t = prop_of_clause c
   21.65                    val by =
   21.66                      By_Metis ([],
   21.67 -                      (fold (add_fact_from_dependencies fact_names)
   21.68 +                      (fold (add_fact_of_dependencies fact_names)
   21.69                              gamma no_facts))
   21.70                    fun prove by = Prove (maybe_show outer c [], l, t, by)
   21.71                    fun do_rest l step =