# HG changeset patch
# User blanchet
# Date 1368704053 -7200
# Node ID 9a92383429637513bac116297941870c41ca2319
# Parent  9f6f0a89d16b4df87e155e04b9c138e6f8348bc2
tuning -- renamed '_from_' to '_of_' in Sledgehammer

diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 16 13:34:13 2013 +0200
@@ -219,7 +219,7 @@
 
 val timing = true;
 fun time timer msg = (if timing
-  then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
+  then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
   else (); Timer.startRealTimer ());
 
 val preN = "pre_"
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Thu May 16 13:34:13 2013 +0200
@@ -108,7 +108,7 @@
 
 fun refute_tptp_file thy timeout file_name =
   let
-    fun print_szs_from_outcome falsify s =
+    fun print_szs_of_outcome falsify s =
       "% SZS status " ^
       (if s = "genuine" then
          if falsify then "CounterSatisfiable" else "Satisfiable"
@@ -122,7 +122,7 @@
   in
     Refute.refute_term ctxt params (defs @ nondefs)
         (case conjs of conj :: _ => conj | [] => @{prop True})
-    |> print_szs_from_outcome (not (null conjs))
+    |> print_szs_of_outcome (not (null conjs))
   end
 
 
@@ -263,7 +263,7 @@
   Logic.list_implies (rev defs @ rev nondefs,
                       case conjs of conj :: _ => conj | [] => @{prop False})
 
-fun print_szs_from_success conjs success =
+fun print_szs_of_success conjs success =
   Output.urgent_message ("% SZS status " ^
                          (if success then
                             if null conjs then "Unsatisfiable" else "Theorem"
@@ -277,7 +277,7 @@
     val conj = make_conj assms conjs
   in
     can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
-    |> print_szs_from_success conjs
+    |> print_szs_of_success conjs
   end
 
 fun generic_isabelle_tptp_file demo thy timeout file_name =
@@ -292,7 +292,7 @@
      can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
      can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
          (atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
-    |> print_szs_from_success conjs
+    |> print_szs_of_success conjs
   end
 
 val isabelle_tptp_file = generic_isabelle_tptp_file false
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Thu May 16 13:34:13 2013 +0200
@@ -157,7 +157,7 @@
   let
     val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
     val type_enc =
-      type_enc |> type_enc_from_string Non_Strict
+      type_enc |> type_enc_of_string Non_Strict
                |> adjust_type_enc format
     val mono = not (is_type_enc_polymorphic type_enc)
     val facts =
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Thu May 16 13:34:13 2013 +0200
@@ -75,7 +75,7 @@
       let val facts = facts |> map (fst o fst) in
         str_of_method method ^
         (if is_none outcome then
-           "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
+           "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
            (used_facts |> map (with_index facts o fst)
                        |> sort (int_ord o pairself fst)
                        |> map index_str
@@ -199,7 +199,7 @@
        "slice" |> not slice ? prefix "dont_",
        "type_enc = " ^ the_default "smart" type_enc,
        "lam_trans = " ^ the_default "smart" lam_trans,
-       "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout),
+       "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val _ = print " * * *";
     val _ = print ("Options: " ^ commas options);
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu May 16 13:34:13 2013 +0200
@@ -87,7 +87,7 @@
   val proxify_const : string -> (string * string) option
   val invert_const : string -> string
   val unproxify_const : string -> string
-  val new_skolem_var_name_from_const : string -> string
+  val new_skolem_var_name_of_const : string -> string
   val atp_logical_consts : string list
   val atp_irrelevant_consts : string list
   val atp_widely_irrelevant_consts : string list
@@ -96,7 +96,7 @@
   val is_type_enc_polymorphic : type_enc -> bool
   val level_of_type_enc : type_enc -> type_level
   val is_type_enc_sound : type_enc -> bool
-  val type_enc_from_string : strictness -> string -> type_enc
+  val type_enc_of_string : strictness -> string -> type_enc
   val adjust_type_enc : atp_format -> type_enc -> type_enc
   val is_lambda_free : term -> bool
   val mk_aconns :
@@ -104,7 +104,7 @@
   val unmangled_const : string -> string * (string, 'b) ho_term list
   val unmangled_const_name : string -> string list
   val helper_table : ((string * bool) * (status * thm) list) list
-  val trans_lams_from_string :
+  val trans_lams_of_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val string_of_status : status -> string
   val factsN : string
@@ -395,7 +395,7 @@
 
 fun make_class clas = class_prefix ^ ascii_of clas
 
-fun new_skolem_var_name_from_const s =
+fun new_skolem_var_name_of_const s =
   let val ss = s |> space_explode Long_Name.separator in
     nth ss (length ss - 2)
   end
@@ -568,18 +568,18 @@
 
 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
    Also accumulates sort infomation. *)
-fun iterm_from_term thy type_enc bs (P $ Q) =
+fun iterm_of_term thy type_enc bs (P $ Q) =
     let
-      val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
-      val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
+      val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
+      val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
-  | iterm_from_term thy type_enc _ (Const (c, T)) =
+  | iterm_of_term thy type_enc _ (Const (c, T)) =
     (IConst (`(make_fixed_const (SOME type_enc)) c, T,
              robust_const_type_args thy (c, T)),
      atomic_types_of T)
-  | iterm_from_term _ _ _ (Free (s, T)) =
+  | iterm_of_term _ _ _ (Free (s, T)) =
     (IConst (`make_fixed_var s, T, []), atomic_types_of T)
-  | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
+  | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
        let
          val Ts = T |> strip_type |> swap |> op ::
@@ -587,15 +587,14 @@
        in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
      else
        IVar ((make_schematic_var v, s), T), atomic_types_of T)
-  | iterm_from_term _ _ bs (Bound j) =
+  | iterm_of_term _ _ bs (Bound j) =
     nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
-  | iterm_from_term thy type_enc bs (Abs (s, T, t)) =
+  | iterm_of_term thy type_enc bs (Abs (s, T, t)) =
     let
       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
       val s = vary s
       val name = `make_bound_var s
-      val (tm, atomic_Ts) =
-        iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
+      val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
 
 (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
@@ -605,7 +604,7 @@
 fun try_unsuffixes ss s =
   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
 
-fun type_enc_from_string strictness s =
+fun type_enc_of_string strictness s =
   (case try (unprefix "tc_") s of
      SOME s => (SOME Type_Class_Polymorphic, s)
    | NONE =>
@@ -903,7 +902,7 @@
 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
 val fused_infinite_type = Type (fused_infinite_type_name, [])
 
-fun raw_ho_type_from_typ type_enc =
+fun raw_ho_type_of_typ type_enc =
   let
     fun term (Type (s, Ts)) =
       AType (case (is_type_enc_higher_order type_enc, s) of
@@ -919,11 +918,12 @@
     | term (TVar z) = AType (tvar_name z, [])
   in term end
 
-fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
-  | ho_term_from_ho_type _ = raise Fail "unexpected type"
+fun ho_term_of_ho_type (AType (name, tys)) =
+    ATerm ((name, []), map ho_term_of_ho_type tys)
+  | ho_term_of_ho_type _ = raise Fail "unexpected type"
 
 fun ho_type_of_type_arg type_enc T =
-  if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T)
+  if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T)
 
 (* This shouldn't clash with anything else. *)
 val uncurried_alias_sep = "\000"
@@ -938,7 +938,7 @@
   | generic_mangled_type_name _ _ = raise Fail "unexpected type"
 
 fun mangled_type type_enc =
-  generic_mangled_type_name fst o raw_ho_type_from_typ type_enc
+  generic_mangled_type_name fst o raw_ho_type_of_typ type_enc
 
 fun make_native_type s =
   if s = tptp_bool_type orelse s = tptp_fun_type orelse
@@ -947,7 +947,7 @@
   else
     native_type_prefix ^ ascii_of s
 
-fun native_ho_type_from_raw_ho_type type_enc pred_sym ary =
+fun native_ho_type_of_raw_ho_type type_enc pred_sym ary =
   let
     fun to_mangled_atype ty =
       AType ((make_native_type (generic_mangled_type_name fst ty),
@@ -967,9 +967,9 @@
       | to_ho _ = raise Fail "unexpected type"
   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
 
-fun native_ho_type_from_typ type_enc pred_sym ary =
-  native_ho_type_from_raw_ho_type type_enc pred_sym ary
-  o raw_ho_type_from_typ type_enc
+fun native_ho_type_of_typ type_enc pred_sym ary =
+  native_ho_type_of_raw_ho_type type_enc pred_sym ary
+  o raw_ho_type_of_typ type_enc
 
 (* Make atoms for sorted type variables. *)
 fun generic_add_sorts_on_type _ [] = I
@@ -983,9 +983,9 @@
 
 fun process_type_args type_enc T_args =
   if is_type_enc_native type_enc then
-    (map (native_ho_type_from_typ type_enc false 0) T_args, [])
+    (map (native_ho_type_of_typ type_enc false 0) T_args, [])
   else
-    ([], map_filter (Option.map ho_term_from_ho_type
+    ([], map_filter (Option.map ho_term_of_ho_type
                      o ho_type_of_type_arg type_enc) T_args)
 
 fun class_atom type_enc (cl, T) =
@@ -1194,11 +1194,11 @@
       | filt _ tm = tm
   in filt 0 end
 
-fun iformula_from_prop ctxt type_enc iff_for_eq =
+fun iformula_of_prop ctxt type_enc iff_for_eq =
   let
     val thy = Proof_Context.theory_of ctxt
     fun do_term bs t atomic_Ts =
-      iterm_from_term thy type_enc bs (Envir.eta_contract t)
+      iterm_of_term thy type_enc bs (Envir.eta_contract t)
       |>> (introduce_proxies_in_iterm type_enc
            #> mangle_type_args_in_iterm type_enc #> AAtom)
       ||> union (op =) atomic_Ts
@@ -1297,8 +1297,7 @@
   let
     val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
     val (iformula, atomic_Ts) =
-      iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
-                         []
+      iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
       |>> close_universally add_iterm_vars
   in
     {name = name, stature = stature, role = role, iformula = iformula,
@@ -1903,7 +1902,7 @@
     end
   | extract_lambda_def _ = raise Fail "malformed lifted lambda"
 
-fun trans_lams_from_string ctxt type_enc lam_trans =
+fun trans_lams_of_string ctxt type_enc lam_trans =
   if lam_trans = no_lamsN then
     rpair []
   else if lam_trans = hide_lamsN then
@@ -1955,7 +1954,7 @@
                        concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
-    val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
+    val trans_lams = trans_lams_of_string ctxt type_enc lam_trans
     val fact_ts = facts |> map snd
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
@@ -2058,17 +2057,17 @@
 fun do_bound_type ctxt mono type_enc =
   case type_enc of
     Native (_, _, level) =>
-    fused_type ctxt mono level 0 #> native_ho_type_from_typ type_enc false 0
+    fused_type ctxt mono level 0 #> native_ho_type_of_typ type_enc false 0
     #> SOME
   | _ => K NONE
 
 fun tag_with_type ctxt mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
   |> mangle_type_args_in_iterm type_enc
-  |> ho_term_from_iterm ctxt mono type_enc pos
+  |> ho_term_of_iterm ctxt mono type_enc pos
   |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt mono type_enc pos =
+and ho_term_of_iterm ctxt mono type_enc pos =
   let
     fun term site u =
       let
@@ -2094,7 +2093,7 @@
             map (term Elsewhere) args |> mk_aterm type_enc name []
           | IAbs ((name, T), tm) =>
             if is_type_enc_higher_order type_enc then
-              AAbs (((name, native_ho_type_from_typ type_enc true 0 T), (* FIXME? why "true"? *)
+              AAbs (((name, native_ho_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
                      term Elsewhere tm), map (term Elsewhere) args)
             else
               raise Fail "unexpected lambda-abstraction"
@@ -2102,11 +2101,11 @@
         val tag = should_tag_with_type ctxt mono type_enc site u T
       in t |> tag ? tag_with_type ctxt mono type_enc pos T end
   in term (Top_Level pos) end
-and formula_from_iformula ctxt mono type_enc should_guard_var =
+and formula_of_iformula ctxt mono type_enc should_guard_var =
   let
     val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
-    val do_term = ho_term_from_iterm ctxt mono type_enc
+    val do_term = ho_term_of_iterm ctxt mono type_enc
     fun do_out_of_bound_type pos phi universal (name, T) =
       if should_guard_type ctxt mono type_enc
              (fn () => should_guard_var thy level pos phi universal name) T then
@@ -2121,7 +2120,7 @@
       else
         NONE
     fun do_formula pos (ATyQuant (q, xs, phi)) =
-        ATyQuant (q, map (apfst (native_ho_type_from_typ type_enc false 0)) xs,
+        ATyQuant (q, map (apfst (native_ho_type_of_typ type_enc false 0)) xs,
                   do_formula pos phi)
       | do_formula pos (AQuant (q, xs, phi)) =
         let
@@ -2161,7 +2160,7 @@
             encode name, alt name),
            role,
            iformula
-           |> formula_from_iformula ctxt mono type_enc
+           |> formula_of_iformula ctxt mono type_enc
                   should_guard_var_in_formula (if pos then SOME true else NONE)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types,
@@ -2188,7 +2187,7 @@
                 map (fn (cls, T) =>
                         (T |> dest_TVar |> tvar_name, map (`make_class) cls))
                     prems,
-                native_ho_type_from_typ type_enc false 0 T, `make_class cl)
+                native_ho_type_of_typ type_enc false 0 T, `make_class cl)
   else
     Formula ((tcon_clause_prefix ^ name, ""), Axiom,
              mk_ahorn (maps (class_atoms type_enc) prems)
@@ -2200,7 +2199,7 @@
                        ({name, role, iformula, atomic_types, ...} : ifact) =
   Formula ((conjecture_prefix ^ name, ""), role,
            iformula
-           |> formula_from_iformula ctxt mono type_enc
+           |> formula_of_iformula ctxt mono type_enc
                   should_guard_var_in_formula (SOME false)
            |> close_formula_universally
            |> bound_tvars type_enc true atomic_types, NONE, [])
@@ -2213,8 +2212,7 @@
       fun line j (cl, T) =
         if type_classes then
           Class_Memb (class_memb_prefix ^ string_of_int j, [],
-                      native_ho_type_from_typ type_enc false 0 T,
-                      `make_class cl)
+                      native_ho_type_of_typ type_enc false 0 T, `make_class cl)
         else
           Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
                    class_atom type_enc (cl, T), NONE, [])
@@ -2386,8 +2384,8 @@
            IConst (`make_bound_var "X", T, [])
            |> type_guard_iterm type_enc T
            |> AAtom
-           |> formula_from_iformula ctxt mono type_enc
-                                    always_guard_var_in_formula (SOME true)
+           |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula
+                                  (SOME true)
            |> close_formula_universally
            |> bound_tvars type_enc true (atomic_types_of T),
            NONE, isabelle_info inductiveN helper_rank)
@@ -2423,7 +2421,7 @@
   in
     Sym_Decl (sym_decl_prefix ^ s, (s, s'),
               T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
-                |> native_ho_type_from_typ type_enc pred_sym ary
+                |> native_ho_type_of_typ type_enc pred_sym ary
                 |> not (null T_args)
                    ? curry APi (map (tvar_name o dest_TVar) T_args))
   end
@@ -2456,8 +2454,8 @@
              |> fold (curry (IApp o swap)) bounds
              |> type_guard_iterm type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_iformula ctxt mono type_enc
-                                      always_guard_var_in_formula (SOME true)
+             |> formula_of_iformula ctxt mono type_enc
+                                    always_guard_var_in_formula (SOME true)
              |> close_formula_universally
              |> bound_tvars type_enc (n > 1) (atomic_types_of T)
              |> maybe_negate,
@@ -2544,15 +2542,15 @@
                            (type_enc as Native (_, _, level)) sym_tab =
     let
       val thy = Proof_Context.theory_of ctxt
-      val ho_term_from_term =
-        iterm_from_term thy type_enc []
-        #> fst #> ho_term_from_iterm ctxt mono type_enc NONE
+      val ho_term_of_term =
+        iterm_of_term thy type_enc []
+        #> fst #> ho_term_of_iterm ctxt mono type_enc NONE
     in
       if is_type_enc_polymorphic type_enc then
-        [(native_ho_type_from_typ type_enc false 0 @{typ nat},
-          map ho_term_from_term [@{term "0::nat"}, @{term Suc}], true) (*,
-         (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
-          map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
+        [(native_ho_type_of_typ type_enc false 0 @{typ nat},
+          map ho_term_of_term [@{term "0::nat"}, @{term Suc}], true) (*,
+         (native_ho_type_of_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
+          map (ho_term_of_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
           true) *)]
       else
         []
@@ -2584,7 +2582,7 @@
         val base_ary = min_ary_of sym_tab0 base_s
         fun do_const name = IConst (name, T, T_args)
         val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc
-        val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
+        val ho_term_of = ho_term_of_iterm ctxt mono type_enc (SOME true)
         val name1 as (s1, _) =
           base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
         val name2 as (s2, _) = base_name |> aliased_uncurried ary
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu May 16 13:34:13 2013 +0200
@@ -55,7 +55,7 @@
   val parse_formula :
     string list
     -> (string, 'a, (string, 'a) ho_term, string) formula * string list
-  val atp_proof_from_tstplike_proof : string problem -> string -> string proof
+  val atp_proof_of_tstplike_proof : string problem -> string -> string proof
   val clean_up_atp_proof_dependencies : string proof -> string proof
   val map_term_names_in_atp_proof :
     (string -> string) -> string proof -> string proof
@@ -493,8 +493,8 @@
                          (Scan.repeat1 (parse_line problem))))
   #> fst
 
-fun atp_proof_from_tstplike_proof _ "" = []
-  | atp_proof_from_tstplike_proof problem tstp =
+fun atp_proof_of_tstplike_proof _ "" = []
+  | atp_proof_of_tstplike_proof problem tstp =
     tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
     |> parse_proof problem
     |> sort (step_name_ord o pairself #1)
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
@@ -26,10 +26,10 @@
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
   val unalias_type_enc : string -> string list
-  val term_from_atp :
+  val term_of_atp :
     Proof.context -> bool -> int Symtab.table -> typ option ->
     (string, string) ho_term -> term
-  val prop_from_atp :
+  val prop_of_atp :
     Proof.context -> bool -> int Symtab.table ->
     (string, string, (string, string) ho_term, string) formula -> term
 end;
@@ -97,8 +97,8 @@
 
 (* Type variables are given the basic sort "HOL.type". Some will later be
    constrained by information from type literals, or by type inference. *)
-fun typ_from_atp ctxt (u as ATerm ((a, _), us)) =
-  let val Ts = map (typ_from_atp ctxt) us in
+fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =
+  let val Ts = map (typ_of_atp ctxt) us in
     case unprefix_and_unascii type_const_prefix a of
       SOME b => Type (invert_const b, Ts)
     | NONE =>
@@ -117,8 +117,8 @@
 
 (* Type class literal applied to a type. Returns triple of polarity, class,
    type. *)
-fun type_constraint_from_term ctxt (u as ATerm ((a, _), us)) =
-  case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
+fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) =
+  case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of
     (SOME b, [T]) => (b, T)
   | _ => raise HO_TERM [u]
 
@@ -166,7 +166,7 @@
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
-fun term_from_atp ctxt textual sym_tab =
+fun term_of_atp ctxt textual sym_tab =
   let
     val thy = Proof_Context.theory_of ctxt
     (* For Metis, we use 1 rather than 0 because variable references in clauses
@@ -198,7 +198,7 @@
             if s' = type_tag_name then
               case mangled_us @ us of
                 [typ_u, term_u] =>
-                do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
+                do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u
               | _ => raise HO_TERM us
             else if s' = predicator_name then
               do_term [] (SOME @{typ bool}) (hd us)
@@ -223,7 +223,7 @@
                 val T =
                   (if not (null type_us) andalso
                       num_type_args thy s' = length type_us then
-                     let val Ts = type_us |> map (typ_from_atp ctxt) in
+                     let val Ts = type_us |> map (typ_of_atp ctxt) in
                        if new_skolem then
                          SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
                        else if textual then
@@ -240,7 +240,7 @@
                                   | NONE => HOLogic.typeT))
                 val t =
                   if new_skolem then
-                    Var ((new_skolem_var_name_from_const s'', var_index), T)
+                    Var ((new_skolem_var_name_of_const s'', var_index), T)
                   else
                     Const (unproxify_const s', T)
               in list_comb (t, term_ts @ extra_ts) end
@@ -277,12 +277,12 @@
           in list_comb (t, ts) end
   in do_term [] end
 
-fun term_from_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
+fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
   if String.isPrefix class_prefix s then
-    add_type_constraint pos (type_constraint_from_term ctxt u)
+    add_type_constraint pos (type_constraint_of_term ctxt u)
     #> pair @{const True}
   else
-    pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
+    pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
 
 (* Update schematic type variables with detected sort constraints. It's not
    totally clear whether this code is necessary. *)
@@ -308,7 +308,7 @@
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)
-fun prop_from_atp ctxt textual sym_tab phi =
+fun prop_of_atp ctxt textual sym_tab phi =
   let
     fun do_formula pos phi =
       case phi of
@@ -329,7 +329,7 @@
              | AImplies => s_imp
              | AIff => s_iff
              | ANot => raise Fail "impossible connective")
-      | AAtom tm => term_from_atom ctxt textual sym_tab pos tm
+      | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
       | _ => raise FORMULA [phi]
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
 
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Thu May 16 13:34:13 2013 +0200
@@ -17,8 +17,8 @@
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
-  val string_from_ext_time : bool * Time.time -> string
-  val string_from_time : Time.time -> string
+  val string_of_ext_time : bool * Time.time -> string
+  val string_of_time : Time.time -> string
   val type_instance : theory -> typ -> typ -> bool
   val type_generalization : theory -> typ -> typ -> bool
   val type_intersect : theory -> typ -> typ -> bool
@@ -134,7 +134,7 @@
            Keyword.is_keyword s) ? quote
   end
 
-fun string_from_ext_time (plus, time) =
+fun string_of_ext_time (plus, time) =
   let val ms = Time.toMilliseconds time in
     (if plus then "> " else "") ^
     (if plus andalso ms mod 1000 = 0 then
@@ -145,7 +145,7 @@
        string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
   end
 
-val string_from_time = string_from_ext_time o pair false
+val string_of_time = string_of_ext_time o pair false
 
 fun type_instance thy T T' = Sign.typ_instance thy (T, T')
 fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Meson/meson_clausify.ML
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu May 16 13:34:13 2013 +0200
@@ -191,7 +191,7 @@
 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
-fun old_skolem_theorem_from_def thy rhs0 =
+fun old_skolem_theorem_of_def thy rhs0 =
   let
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
@@ -200,7 +200,7 @@
     val T =
       case hilbert of
         Const (_, Type (@{type_name fun}, [_, T])) => T
-      | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
+      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
                          [hilbert])
     val cex = cterm_of thy (HOLogic.exists_const T)
     val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
@@ -372,7 +372,7 @@
       nnf_axiom choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
       make_cnf (if new_skolem orelse null choice_ths then []
-                else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
+                else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
                th ctxt ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu May 16 13:34:13 2013 +0200
@@ -138,7 +138,7 @@
 val prepare_helper =
   Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
 
-fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
+fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
   if is_tptp_variable s then
     Metis_Term.Var (Metis_Name.fromString s)
   else
@@ -147,24 +147,23 @@
      | NONE => (s, false))
     |> (fn (s, swap) =>
            Metis_Term.Fn (Metis_Name.fromString s,
-                          tms |> map (metis_term_from_atp type_enc)
+                          tms |> map (metis_term_of_atp type_enc)
                               |> swap ? rev))
-fun metis_atom_from_atp type_enc (AAtom tm) =
-    (case metis_term_from_atp type_enc tm of
+fun metis_atom_of_atp type_enc (AAtom tm) =
+    (case metis_term_of_atp type_enc tm of
        Metis_Term.Fn x => x
      | _ => raise Fail "non CNF -- expected function")
-  | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
-fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
-    (false, metis_atom_from_atp type_enc phi)
-  | metis_literal_from_atp type_enc phi =
-    (true, metis_atom_from_atp type_enc phi)
-fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
-    maps (metis_literals_from_atp type_enc) phis
-  | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
-fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
+  | metis_atom_of_atp _ _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_of_atp type_enc (AConn (ANot, [phi])) =
+    (false, metis_atom_of_atp type_enc phi)
+  | metis_literal_of_atp type_enc phi = (true, metis_atom_of_atp type_enc phi)
+fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
+    maps (metis_literals_of_atp type_enc) phis
+  | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
+fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
     let
       fun some isa =
-        SOME (phi |> metis_literals_from_atp type_enc
+        SOME (phi |> metis_literals_of_atp type_enc
                   |> Metis_LiteralSet.fromList
                   |> Metis_Thm.axiom, isa)
     in
@@ -197,7 +196,7 @@
         end
       | NONE => TrueI |> Isa_Raw |> some
     end
-  | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
+  | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
 
 fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
     eliminate_lam_wrappers t
@@ -251,7 +250,7 @@
     (* "rev" is for compatibility with existing proof scripts. *)
     val axioms =
       atp_problem
-      |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
+      |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
     fun ord_info () = atp_problem_term_order_info atp_problem
   in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
 
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
@@ -13,7 +13,7 @@
 
   exception METIS_RECONSTRUCT of string * string
 
-  val hol_clause_from_metis :
+  val hol_clause_of_metis :
     Proof.context -> type_enc -> int Symtab.table
     -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
   val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
@@ -36,40 +36,40 @@
 
 exception METIS_RECONSTRUCT of string * string
 
-fun atp_name_from_metis type_enc s =
+fun atp_name_of_metis type_enc s =
   case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
     SOME ((s, _), (_, swap)) => (s, swap)
   | _ => (s, false)
-fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
-    let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
-      ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
+fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
+    let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
+      ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
     end
-  | atp_term_from_metis _ (Metis_Term.Var s) =
+  | atp_term_of_metis _ (Metis_Term.Var s) =
     ATerm ((Metis_Name.toString s, []), [])
 
-fun hol_term_from_metis ctxt type_enc sym_tab =
-  atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
+fun hol_term_of_metis ctxt type_enc sym_tab =
+  atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
 
-fun atp_literal_from_metis type_enc (pos, atom) =
-  atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
+fun atp_literal_of_metis type_enc (pos, atom) =
+  atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
        |> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
-  | atp_clause_from_metis type_enc lits =
-    lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
+fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
+  | atp_clause_of_metis type_enc lits =
+    lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
 
 fun polish_hol_terms ctxt (lifted, old_skolems) =
   map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
   #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
 
-fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
+fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
   Metis_Thm.clause
   #> Metis_LiteralSet.toList
-  #> atp_clause_from_metis type_enc
-  #> prop_from_atp ctxt false sym_tab
+  #> atp_clause_of_metis type_enc
+  #> prop_of_atp ctxt false sym_tab
   #> singleton (polish_hol_terms ctxt concealed)
 
-fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
-  let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
+fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
+  let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
       val _ = trace_msg ctxt (fn () => "  calling type inference:")
       val _ = app (fn t => trace_msg ctxt
                                      (fn () => Syntax.string_of_term ctxt t)) ts
@@ -102,7 +102,7 @@
 (* INFERENCE RULE: AXIOM *)
 
 (* This causes variables to have an index of 1 by default. See also
-   "term_from_atp" in "ATP_Proof_Reconstruct". *)
+   "term_of_atp" in "ATP_Proof_Reconstruct". *)
 val axiom_inference = Thm.incr_indexes 1 oo lookth
 
 (* INFERENCE RULE: ASSUME *)
@@ -118,7 +118,7 @@
 fun assume_inference ctxt type_enc concealed sym_tab atom =
   inst_excluded_middle
       (Proof_Context.theory_of ctxt)
-      (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
+      (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
                  (Metis_Term.Fn atom))
 
 (* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -134,14 +134,14 @@
       fun subst_translation (x,y) =
         let val v = find_var x
             (* We call "polish_hol_terms" below. *)
-            val t = hol_term_from_metis ctxt type_enc sym_tab y
+            val t = hol_term_of_metis ctxt type_enc sym_tab y
         in  SOME (cterm_of thy (Var v), t)  end
         handle Option.Option =>
                (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
                                          " in " ^ Display.string_of_thm ctxt i_th);
                 NONE)
              | TYPE _ =>
-               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
+               (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^
                                          " in " ^ Display.string_of_thm ctxt i_th);
                 NONE)
       fun remove_typeinst (a, t) =
@@ -275,7 +275,7 @@
       let
         val thy = Proof_Context.theory_of ctxt
         val i_atom =
-          singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
+          singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
                     (Metis_Term.Fn atom)
         val _ = trace_msg ctxt (fn () =>
                     "  atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -309,7 +309,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val i_t =
-      singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
+      singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
     val c_t = cterm_incr_types thy refl_idx i_t
   in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -323,7 +323,7 @@
   let val thy = Proof_Context.theory_of ctxt
       val m_tm = Metis_Term.Fn atom
       val [i_atom, i_tm] =
-        hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
+        hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
       val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
       fun replace_item_list lx 0 (_::ls) = lx::ls
         | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu May 16 13:34:13 2013 +0200
@@ -47,9 +47,9 @@
    "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
@@ -62,11 +62,11 @@
   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
 
@@ -158,13 +158,13 @@
       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")
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 16 13:34:13 2013 +0200
@@ -1051,7 +1051,7 @@
              (print_nt (fn () => excipit "ran out of time after checking");
               if !met_potential > 0 then potentialN else unknownN)
     val _ = print_v (fn () =>
-                "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
+                "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
                 ".")
   in (outcome_code, !state_ref) end
 
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu May 16 13:34:13 2013 +0200
@@ -52,7 +52,7 @@
   val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
-  val string_from_time : Time.time -> string
+  val string_of_time : Time.time -> string
   val nat_subscript : int -> string
   val flip_polarity : polarity -> polarity
   val prop_T : typ
@@ -237,7 +237,7 @@
 
 val parse_bool_option = Sledgehammer_Util.parse_bool_option
 val parse_time_option = Sledgehammer_Util.parse_time_option
-val string_from_time = ATP_Util.string_from_time
+val string_of_time = ATP_Util.string_of_time
 
 val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
 fun nat_subscript n =
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu May 16 13:34:13 2013 +0200
@@ -21,7 +21,7 @@
   val ignore_no_atp : bool Config.T
   val instantiate_inducts : bool Config.T
   val no_fact_override : fact_override
-  val fact_from_ref :
+  val fact_of_ref :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
   val backquote_thm : Proof.context -> thm -> string
@@ -119,7 +119,7 @@
 fun stature_of_thm global assms chained css name th =
   (scope_of_thm global assms chained th, status_of_thm css name th)
 
-fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
+fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
   let
     val ths = Attrib.eval_thms ctxt [xthm]
     val bracket =
@@ -502,7 +502,7 @@
     in
       (if only then
          maps (map (fn ((name, stature), th) => ((K name, stature), th))
-               o fact_from_ref ctxt reserved chained css) add
+               o fact_of_ref ctxt reserved chained css) add
        else
          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
            all_facts ctxt false ho_atp reserved add chained css
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 16 13:34:13 2013 +0200
@@ -159,7 +159,7 @@
                             | _ => value)
     | NONE => (name, value)
 
-val any_type_enc = type_enc_from_string Strict "erased"
+val any_type_enc = type_enc_of_string Strict "erased"
 
 (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
    can be omitted. For the last four, this is a secret feature. *)
@@ -171,9 +171,9 @@
          else if null value then
            if is_prover_list ctxt name then
              ("provers", [name])
-           else if can (type_enc_from_string Strict) name then
+           else if can (type_enc_of_string Strict) name then
              ("type_enc", [name])
-           else if can (trans_lams_from_string ctxt any_type_enc) name then
+           else if can (trans_lams_of_string ctxt any_type_enc) name then
              ("lam_trans", [name])
            else if member (op =) fact_filters name then
              ("fact_filter", [name])
@@ -295,7 +295,7 @@
         NONE
       else case lookup_string "type_enc" of
         "smart" => NONE
-      | s => (type_enc_from_string Strict s; SOME s)
+      | s => (type_enc_of_string Strict s; SOME s)
     val strict = mode = Auto_Try orelse lookup_bool "strict"
     val lam_trans = lookup_option lookup_string "lam_trans"
     val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu May 16 13:34:13 2013 +0200
@@ -1024,7 +1024,7 @@
                "Learned " ^ string_of_int num_proofs ^ " " ^
                (if run_prover then "automatic" else "Isar") ^ " proof" ^
                plural_s num_proofs ^ " in the last " ^
-               string_from_time commit_timeout ^ "."
+               string_of_time commit_timeout ^ "."
                |> Output.urgent_message
              end
            else
@@ -1111,10 +1111,8 @@
         if verbose orelse auto_level < 2 then
           "Learned " ^ string_of_int n ^ " nontrivial " ^
           (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
-          (if verbose then
-             " in " ^ string_from_time (Timer.checkRealTimer timer)
-           else
-             "") ^ "."
+          (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
+           else "") ^ "."
         else
           ""
       end
@@ -1138,7 +1136,7 @@
       ("MaShing through " ^ string_of_int num_facts ^ " fact" ^
        plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
        (case timeout of
-          SOME timeout => " timeout: " ^ string_from_time timeout
+          SOME timeout => " timeout: " ^ string_of_time timeout
         | NONE => "") ^ ").\n\nCollecting Isar proofs first..."
        |> Output.urgent_message;
        learn 1 false;
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu May 16 13:34:13 2013 +0200
@@ -65,7 +65,7 @@
           "Testing " ^ n_facts (map fst facts) ^
           (if verbose then
              case timeout of
-               SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+               SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")"
              | _ => ""
            else
              "") ^ "...")
@@ -96,7 +96,7 @@
                 "Found proof" ^
                  (if length used_facts = length facts then ""
                   else " with " ^ n_facts used_facts) ^
-                 " (" ^ string_from_time run_time ^ ").");
+                 " (" ^ string_of_time run_time ^ ").");
     result
   end
 
@@ -351,7 +351,7 @@
     val css = clasimpset_rule_table_of ctxt
     val facts =
       refs |> maps (map (apsnd single)
-                    o fact_from_ref ctxt reserved chained_ths css)
+                    o fact_of_ref ctxt reserved chained_ths css)
   in
     case subgoal_count state of
       0 => Output.urgent_message "No subgoal!"
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Thu May 16 13:34:13 2013 +0200
@@ -36,7 +36,7 @@
 
 fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
 
-val string_of_preplay_time = ATP_Util.string_from_ext_time
+val string_of_preplay_time = ATP_Util.string_of_ext_time
 
 (* preplay tracing *)
 fun preplay_trace ctxt assms concl time =
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu May 16 13:34:13 2013 +0200
@@ -530,7 +530,7 @@
                 if verbose then
                   "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
                   (case timeout of
-                     SOME timeout => " for " ^ string_from_time timeout
+                     SOME timeout => " for " ^ string_of_time timeout
                    | NONE => "") ^ "..."
                   |> Output.urgent_message
                 else
@@ -616,7 +616,7 @@
 
 fun choose_type_enc soundness best_type_enc format =
   the_default best_type_enc
-  #> type_enc_from_string soundness
+  #> type_enc_of_string soundness
   #> adjust_type_enc format
 
 fun isar_proof_reconstructor ctxt name =
@@ -793,7 +793,7 @@
                 " with " ^ string_of_int num_facts ^ " fact" ^
                 plural_s num_facts ^
                 (case slice_timeout of
-                   SOME timeout => " for " ^ string_from_time timeout
+                   SOME timeout => " for " ^ string_of_time timeout
                  | NONE => "") ^ "..."
                 |> Output.urgent_message
               else
@@ -849,7 +849,7 @@
                      (accum, facts,
                       extract_tstplike_proof_and_outcome verbose proof_delims
                                                          known_failures output
-                      |>> atp_proof_from_tstplike_proof atp_problem
+                      |>> atp_proof_of_tstplike_proof atp_problem
                       handle UNRECOGNIZED_ATP_PROOF () =>
                              ([], SOME ProofIncomplete)))
               handle TimeLimit.TimeOut =>
@@ -921,7 +921,7 @@
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val reconstrs =
             bunch_of_reconstructors needs_full_types
-                (lam_trans_from_atp_proof atp_proof
+                (lam_trans_of_atp_proof atp_proof
                  o (fn desperate => if desperate then hide_lamsN
                                     else metis_default_lam_trans))
         in
@@ -955,7 +955,7 @@
                            one_line_params
               end,
            (if verbose then
-              "\nATP real CPU time: " ^ string_from_time run_time ^ "."
+              "\nATP real CPU time: " ^ string_of_time run_time ^ "."
             else
               "") ^
            (if important_message <> "" then
@@ -991,17 +991,16 @@
    (139, Crashed)]
 val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
 
-fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
+fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
     if is_real_cex then Unprovable else GaveUp
-  | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
-  | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
+  | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
+  | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
     (case AList.lookup (op =) smt_failures code of
        SOME failure => failure
      | NONE => UnknownError ("Abnormal termination with exit code " ^
                              string_of_int code ^ "."))
-  | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
-  | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
-    UnknownError msg
+  | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
+  | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
 
 (* FUDGE *)
 val smt_max_slices =
@@ -1059,7 +1058,7 @@
             quote name ^ " slice " ^ string_of_int slice ^ " with " ^
             string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
             (case slice_timeout of
-               SOME timeout => " for " ^ string_from_time timeout
+               SOME timeout => " for " ^ string_of_time timeout
              | NONE => "") ^ "..."
             |> Output.urgent_message
           else
@@ -1112,7 +1111,7 @@
               if verbose andalso is_some outcome then
                 quote name ^ " invoked with " ^
                 num_of_facts fact_filter num_facts ^ ": " ^
-                string_of_failure (failure_from_smt_failure (the outcome)) ^
+                string_of_failure (failure_of_smt_failure (the outcome)) ^
                 " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
                 "..."
                 |> Output.urgent_message
@@ -1142,7 +1141,7 @@
     val {outcome, used_facts = used_pairs, used_from, run_time} =
       smt_filter_loop name params state goal subgoal weighted_factss
     val used_facts = used_pairs |> map fst
-    val outcome = outcome |> Option.map failure_from_smt_failure
+    val outcome = outcome |> Option.map failure_of_smt_failure
     val (preplay, message, message_tail) =
       case outcome of
         NONE =>
@@ -1161,7 +1160,7 @@
               val num_chained = length (#facts (Proof.goal state))
             in one_line_proof_text num_chained one_line_params end,
          if verbose then
-           "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
+           "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
          else
            "")
       | SOME failure =>
diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu May 16 13:34:13 2013 +0200
@@ -28,7 +28,7 @@
 
   val smtN : string
   val string_of_reconstructor : reconstructor -> string
-  val lam_trans_from_atp_proof : string proof -> string -> string
+  val lam_trans_of_atp_proof : string proof -> string -> string
   val is_typed_helper_used_in_atp_proof : string proof -> bool
   val used_facts_in_atp_proof :
     Proof.context -> (string * stature) list vector -> string proof ->
@@ -121,7 +121,7 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
-fun lam_trans_from_atp_proof atp_proof default =
+fun lam_trans_of_atp_proof atp_proof default =
   case (is_axiom_used_in_proof is_combinator_def atp_proof,
         is_axiom_used_in_proof is_lam_lifted atp_proof) of
     (false, false) => default
@@ -190,7 +190,7 @@
 (** one-liner reconstructor proofs **)
 
 fun show_time NONE = ""
-  | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
+  | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
 
 (* FIXME: Various bugs, esp. with "unfolding"
 fun unusing_chained_facts _ 0 = ""
@@ -279,12 +279,12 @@
   | label_of_clause c =
     (space_implode "___" (map (fst o raw_label_of_name) c), 0)
 
-fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
+fun add_fact_of_dependencies fact_names (names as [(_, ss)]) =
     if is_fact fact_names ss then
       apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
     else
       apfst (insert (op =) (label_of_clause names))
-  | add_fact_from_dependencies fact_names names =
+  | add_fact_of_dependencies fact_names names =
     apfst (insert (op =) (label_of_clause names))
 
 fun repair_name "$true" = "c_True"
@@ -325,7 +325,7 @@
 fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
   let
     val thy = Proof_Context.theory_of ctxt
-    val t = u |> prop_from_atp ctxt true sym_tab
+    val t = u |> prop_of_atp ctxt true sym_tab
               |> uncombine_term thy |> infer_formula_types ctxt
   in
     ((name, role, t, rule, deps),
@@ -648,7 +648,7 @@
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
-    val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
+    val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
     val preplay = preplay_timeout <> SOME Time.zeroTime
 
     fun isar_proof_of () =
@@ -744,7 +744,7 @@
                   val t = prop_of_clause c
                   val by =
                     By_Metis ([],
-                      (fold (add_fact_from_dependencies fact_names)
+                      (fold (add_fact_of_dependencies fact_names)
                             gamma no_facts))
                   fun prove by = Prove (maybe_show outer c [], l, t, by)
                   fun do_rest l step =