renamed Sledgehammer functions with 'for' in their names to 'of'
authorblanchet
Wed May 15 17:43:42 2013 +0200 (2013-05-15 ago)
changeset 51998f732a674db1b
parent 51997 8dbe623a7804
child 51999 0c04e4c21eb3
renamed Sledgehammer functions with 'for' in their names to 'of'
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/sledgehammer_tactics.ML
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
src/HOL/Tools/Metis/metis_generate.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_compress.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_mepo.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed May 15 17:27:24 2013 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed May 15 17:43:42 2013 +0200
     1.3 @@ -33,15 +33,15 @@
     1.4  
     1.5  val fact_name_of = prefix fact_prefix o ascii_of
     1.6  
     1.7 -fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN
     1.8 -  | atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN
     1.9 -  | atp_for_format (DFG Polymorphic) = spass_polyN
    1.10 -  | atp_for_format (DFG Monomorphic) = spassN
    1.11 -  | atp_for_format (TFF (Polymorphic, _)) = alt_ergoN
    1.12 -  | atp_for_format (TFF (Monomorphic, _)) = vampireN
    1.13 -  | atp_for_format FOF = eN
    1.14 -  | atp_for_format CNF_UEQ = waldmeisterN
    1.15 -  | atp_for_format CNF = eN
    1.16 +fun atp_of_format (THF (Polymorphic, _, _, _)) = dummy_thfN
    1.17 +  | atp_of_format (THF (Monomorphic, _, _, _)) = satallaxN
    1.18 +  | atp_of_format (DFG Polymorphic) = spass_polyN
    1.19 +  | atp_of_format (DFG Monomorphic) = spassN
    1.20 +  | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN
    1.21 +  | atp_of_format (TFF (Monomorphic, _)) = vampireN
    1.22 +  | atp_of_format FOF = eN
    1.23 +  | atp_of_format CNF_UEQ = waldmeisterN
    1.24 +  | atp_of_format CNF = eN
    1.25  
    1.26  val atp_timeout = seconds 0.5
    1.27  
    1.28 @@ -49,11 +49,11 @@
    1.29    let
    1.30      val thy = Proof_Context.theory_of ctxt
    1.31      val prob_file = File.tmp_path (Path.explode "prob")
    1.32 -    val atp = atp_for_format format
    1.33 +    val atp = atp_of_format format
    1.34      val {exec, arguments, proof_delims, known_failures, ...} =
    1.35        get_atp thy atp ()
    1.36      val ord = effective_term_order ctxt atp
    1.37 -    val _ = problem |> lines_for_atp_problem format ord (K [])
    1.38 +    val _ = problem |> lines_of_atp_problem format ord (K [])
    1.39                      |> File.write_list prob_file
    1.40      val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
    1.41      val command =
    1.42 @@ -70,7 +70,7 @@
    1.43        tracing ("Ran ATP: " ^
    1.44                 (case outcome of
    1.45                    NONE => "Success"
    1.46 -                | SOME failure => string_for_failure failure))
    1.47 +                | SOME failure => string_of_failure failure))
    1.48    in outcome end
    1.49  
    1.50  fun is_problem_line_reprovable ctxt format prelude axioms deps
    1.51 @@ -138,22 +138,22 @@
    1.52    [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool},
    1.53     @{typ unit}]
    1.54  
    1.55 -fun ground_type_for_tvar _ [] tvar =
    1.56 -    raise TYPE ("ground_type_for_sorts", [TVar tvar], [])
    1.57 -  | ground_type_for_tvar thy (T :: Ts) tvar =
    1.58 +fun ground_type_of_tvar _ [] tvar =
    1.59 +    raise TYPE ("ground_type_of_tvar", [TVar tvar], [])
    1.60 +  | ground_type_of_tvar thy (T :: Ts) tvar =
    1.61      if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T
    1.62 -    else ground_type_for_tvar thy Ts tvar
    1.63 +    else ground_type_of_tvar thy Ts tvar
    1.64  
    1.65  fun monomorphize_term ctxt t =
    1.66    let val thy = Proof_Context.theory_of ctxt in
    1.67 -    t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types))
    1.68 +    t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types))
    1.69      handle TYPE _ => @{prop True}
    1.70    end
    1.71  
    1.72  fun heading_sort_key heading =
    1.73    if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading
    1.74  
    1.75 -fun problem_for_theory ctxt thy format infer_policy type_enc =
    1.76 +fun problem_of_theory ctxt thy format infer_policy type_enc =
    1.77    let
    1.78      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.79      val type_enc =
    1.80 @@ -214,8 +214,8 @@
    1.81      |> order_problem_facts name_ord
    1.82    end
    1.83  
    1.84 -fun lines_for_problem ctxt format =
    1.85 -  lines_for_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
    1.86 +fun lines_of_problem ctxt format =
    1.87 +  lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K [])
    1.88  
    1.89  fun write_lines path ss =
    1.90    let
    1.91 @@ -226,8 +226,8 @@
    1.92  fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc
    1.93                                             file_name =
    1.94    let
    1.95 -    val problem = problem_for_theory ctxt thy format infer_policy type_enc
    1.96 -    val ss = lines_for_problem ctxt format problem
    1.97 +    val problem = problem_of_theory ctxt thy format infer_policy type_enc
    1.98 +    val ss = lines_of_problem ctxt format problem
    1.99    in write_lines (Path.explode file_name) ss end
   1.100  
   1.101  fun ap dir = Path.append dir o Path.explode
   1.102 @@ -296,20 +296,20 @@
   1.103      val include_dir = ap problem_dir include_name
   1.104      val _ = Isabelle_System.mkdir include_dir
   1.105      val (prelude, groups) =
   1.106 -      problem_for_theory ctxt thy format infer_policy type_enc
   1.107 +      problem_of_theory ctxt thy format infer_policy type_enc
   1.108        |> split_last
   1.109        ||> (snd
   1.110             #> chop_maximal_groups (op = o pairself theory_name_of_fact)
   1.111             #> map (`(include_base_name_of_fact o hd)))
   1.112      fun write_prelude () =
   1.113 -      let val ss = lines_for_problem ctxt format prelude in
   1.114 +      let val ss = lines_of_problem ctxt format prelude in
   1.115          File.append file_order_path (prelude_base_name ^ "\n");
   1.116          write_lines (ap include_dir prelude_name) ss
   1.117        end
   1.118      fun write_include_file (base_name, facts) =
   1.119        let
   1.120          val name = base_name ^ include_suffix
   1.121 -        val ss = lines_for_problem ctxt format [(factsN, facts)]
   1.122 +        val ss = lines_of_problem ctxt format [(factsN, facts)]
   1.123        in
   1.124          File.append file_order_path (base_name ^ "\n");
   1.125          write_lines (ap include_dir name) ss
   1.126 @@ -321,7 +321,7 @@
   1.127          write_problem_files n (includes @ [include_line base_name]) [] groups
   1.128        | write_problem_files n includes seen
   1.129                              ((base_name, fact :: facts) :: groups) =
   1.130 -        let val fact_s = tptp_string_for_line format fact in
   1.131 +        let val fact_s = tptp_string_of_line format fact in
   1.132            (if should_generate_problem thy base_name fact then
   1.133               let
   1.134                 val (name, conj) =
   1.135 @@ -329,7 +329,7 @@
   1.136                      Formula ((ident, alt), _, phi, _, _) =>
   1.137                      (problem_name_of base_name n (encode_meta alt),
   1.138                       Formula ((ident, alt), Conjecture, phi, NONE, [])))
   1.139 -               val conj_s = tptp_string_for_line format conj
   1.140 +               val conj_s = tptp_string_of_line format conj
   1.141               in
   1.142                 File.append problem_order_path (name ^ "\n");
   1.143                 write_lines (ap problem_dir name) (seen @ [conj_s])
     2.1 --- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed May 15 17:27:24 2013 +0200
     2.2 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed May 15 17:43:42 2013 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4        default_params ctxt override_params
     2.5      val name = hd provers
     2.6      val prover = get_prover ctxt mode name
     2.7 -    val default_max_facts = default_max_facts_for_prover ctxt slice name
     2.8 +    val default_max_facts = default_max_facts_of_prover ctxt slice name
     2.9      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i
    2.10      val ho_atp = exists (is_ho_atp ctxt) provers
    2.11      val reserved = reserved_isar_keyword_table ()
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:27:24 2013 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed May 15 17:43:42 2013 +0200
     3.3 @@ -126,8 +126,8 @@
     3.4    val formula_map :
     3.5      ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula
     3.6    val is_format_higher_order : atp_format -> bool
     3.7 -  val tptp_string_for_line : atp_format -> string problem_line -> string
     3.8 -  val lines_for_atp_problem :
     3.9 +  val tptp_string_of_line : atp_format -> string problem_line -> string
    3.10 +  val lines_of_atp_problem :
    3.11      atp_format -> term_order -> (unit -> (string * int) list) -> string problem
    3.12      -> string list
    3.13    val ensure_cnf_problem :
    3.14 @@ -331,17 +331,17 @@
    3.15    | is_format_typed (DFG _) = true
    3.16    | is_format_typed _ = false
    3.17  
    3.18 -fun tptp_string_for_role Axiom = "axiom"
    3.19 -  | tptp_string_for_role Definition = "definition"
    3.20 -  | tptp_string_for_role Lemma = "lemma"
    3.21 -  | tptp_string_for_role Hypothesis = "hypothesis"
    3.22 -  | tptp_string_for_role Conjecture = "conjecture"
    3.23 -  | tptp_string_for_role Negated_Conjecture = "negated_conjecture"
    3.24 -  | tptp_string_for_role Plain = "plain"
    3.25 -  | tptp_string_for_role Unknown = "unknown"
    3.26 +fun tptp_string_of_role Axiom = "axiom"
    3.27 +  | tptp_string_of_role Definition = "definition"
    3.28 +  | tptp_string_of_role Lemma = "lemma"
    3.29 +  | tptp_string_of_role Hypothesis = "hypothesis"
    3.30 +  | tptp_string_of_role Conjecture = "conjecture"
    3.31 +  | tptp_string_of_role Negated_Conjecture = "negated_conjecture"
    3.32 +  | tptp_string_of_role Plain = "plain"
    3.33 +  | tptp_string_of_role Unknown = "unknown"
    3.34  
    3.35 -fun tptp_string_for_app _ func [] = func
    3.36 -  | tptp_string_for_app format func args =
    3.37 +fun tptp_string_of_app _ func [] = func
    3.38 +  | tptp_string_of_app format func args =
    3.39      if is_format_higher_order format then
    3.40        "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
    3.41      else
    3.42 @@ -363,7 +363,7 @@
    3.43  val suffix_type_of_types =
    3.44    suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
    3.45  
    3.46 -fun str_for_type format ty =
    3.47 +fun str_of_type format ty =
    3.48    let
    3.49      val dfg = case format of DFG _ => true | _ => false
    3.50      fun str _ (AType (s, [])) =
    3.51 @@ -375,7 +375,7 @@
    3.52                        (if dfg then ", " else " " ^ tptp_product_type ^ " ")
    3.53                 |> (not dfg andalso length ss > 1) ? enclose "(" ")"
    3.54            else
    3.55 -            tptp_string_for_app format s ss
    3.56 +            tptp_string_of_app format s ss
    3.57          end
    3.58        | str rhs (AFun (ty1, ty2)) =
    3.59          (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^
    3.60 @@ -389,96 +389,96 @@
    3.61            str false ty
    3.62    in str true ty end
    3.63  
    3.64 -fun string_for_type (format as THF _) ty = str_for_type format ty
    3.65 -  | string_for_type format ty = str_for_type format (flatten_type ty)
    3.66 +fun string_of_type (format as THF _) ty = str_of_type format ty
    3.67 +  | string_of_type format ty = str_of_type format (flatten_type ty)
    3.68  
    3.69 -fun tptp_string_for_quantifier AForall = tptp_forall
    3.70 -  | tptp_string_for_quantifier AExists = tptp_exists
    3.71 +fun tptp_string_of_quantifier AForall = tptp_forall
    3.72 +  | tptp_string_of_quantifier AExists = tptp_exists
    3.73  
    3.74 -fun tptp_string_for_connective ANot = tptp_not
    3.75 -  | tptp_string_for_connective AAnd = tptp_and
    3.76 -  | tptp_string_for_connective AOr = tptp_or
    3.77 -  | tptp_string_for_connective AImplies = tptp_implies
    3.78 -  | tptp_string_for_connective AIff = tptp_iff
    3.79 +fun tptp_string_of_connective ANot = tptp_not
    3.80 +  | tptp_string_of_connective AAnd = tptp_and
    3.81 +  | tptp_string_of_connective AOr = tptp_or
    3.82 +  | tptp_string_of_connective AImplies = tptp_implies
    3.83 +  | tptp_string_of_connective AIff = tptp_iff
    3.84  
    3.85 -fun string_for_bound_var format (s, ty) =
    3.86 +fun string_of_bound_var format (s, ty) =
    3.87    s ^
    3.88    (if is_format_typed format then
    3.89       " " ^ tptp_has_type ^ " " ^
    3.90       (ty |> the_default (AType (tptp_individual_type, []))
    3.91 -         |> string_for_type format)
    3.92 +         |> string_of_type format)
    3.93     else
    3.94       "")
    3.95  
    3.96 -fun tptp_string_for_term _ (ATerm ((s, []), [])) = s
    3.97 -  | tptp_string_for_term format (ATerm ((s, tys), ts)) =
    3.98 +fun tptp_string_of_term _ (ATerm ((s, []), [])) = s
    3.99 +  | tptp_string_of_term format (ATerm ((s, tys), ts)) =
   3.100      (if s = tptp_empty_list then
   3.101         (* used for lists in the optional "source" field of a derivation *)
   3.102 -       "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]"
   3.103 +       "[" ^ commas (map (tptp_string_of_term format) ts) ^ "]"
   3.104       else if is_tptp_equal s then
   3.105         space_implode (" " ^ tptp_equal ^ " ")
   3.106 -                     (map (tptp_string_for_term format) ts)
   3.107 +                     (map (tptp_string_of_term format) ts)
   3.108         |> is_format_higher_order format ? enclose "(" ")"
   3.109       else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice,
   3.110                  ts) of
   3.111         (true, _, [AAbs (((s', ty), tm), [])]) =>
   3.112         (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
   3.113            possible, to work around LEO-II 1.2.8 parser limitation. *)
   3.114 -       tptp_string_for_formula format
   3.115 +       tptp_string_of_formula format
   3.116             (AQuant (if s = tptp_ho_forall then AForall else AExists,
   3.117                      [(s', SOME ty)], AAtom tm))
   3.118       | (_, true, [AAbs (((s', ty), tm), args)]) =>
   3.119         (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always
   3.120            applied to an abstraction. *)
   3.121 -       tptp_string_for_app format
   3.122 -           (tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
   3.123 -            tptp_string_for_term format tm ^ ""
   3.124 +       tptp_string_of_app format
   3.125 +           (tptp_choice ^ "[" ^ s' ^ " : " ^ string_of_type format ty ^ "]: " ^
   3.126 +            tptp_string_of_term format tm ^ ""
   3.127              |> enclose "(" ")")
   3.128 -           (map (tptp_string_for_term format) args)
   3.129 +           (map (tptp_string_of_term format) args)
   3.130       | _ =>
   3.131 -       tptp_string_for_app format s
   3.132 -           (map (string_for_type format) tys
   3.133 -            @ map (tptp_string_for_term format) ts))
   3.134 -  | tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) =
   3.135 -    tptp_string_for_app format
   3.136 -        ("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
   3.137 -         tptp_string_for_term format tm ^ ")")
   3.138 -        (map (tptp_string_for_term format) args)
   3.139 -  | tptp_string_for_term _ _ =
   3.140 +       tptp_string_of_app format s
   3.141 +           (map (string_of_type format) tys
   3.142 +            @ map (tptp_string_of_term format) ts))
   3.143 +  | tptp_string_of_term (format as THF _) (AAbs (((s, ty), tm), args)) =
   3.144 +    tptp_string_of_app format
   3.145 +        ("(^[" ^ s ^ " : " ^ string_of_type format ty ^ "]: " ^
   3.146 +         tptp_string_of_term format tm ^ ")")
   3.147 +        (map (tptp_string_of_term format) args)
   3.148 +  | tptp_string_of_term _ _ =
   3.149      raise Fail "unexpected term in first-order format"
   3.150 -and tptp_string_for_formula format (ATyQuant (q, xs, phi)) =
   3.151 -    tptp_string_for_quantifier q ^
   3.152 +and tptp_string_of_formula format (ATyQuant (q, xs, phi)) =
   3.153 +    tptp_string_of_quantifier q ^
   3.154      "[" ^
   3.155 -    commas (map (suffix_type_of_types o string_for_type format o fst) xs) ^
   3.156 -    "]: " ^ tptp_string_for_formula format phi
   3.157 +    commas (map (suffix_type_of_types o string_of_type format o fst) xs) ^
   3.158 +    "]: " ^ tptp_string_of_formula format phi
   3.159      |> enclose "(" ")"
   3.160 -  | tptp_string_for_formula format (AQuant (q, xs, phi)) =
   3.161 -    tptp_string_for_quantifier q ^
   3.162 -    "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^
   3.163 -    tptp_string_for_formula format phi
   3.164 +  | tptp_string_of_formula format (AQuant (q, xs, phi)) =
   3.165 +    tptp_string_of_quantifier q ^
   3.166 +    "[" ^ commas (map (string_of_bound_var format) xs) ^ "]: " ^
   3.167 +    tptp_string_of_formula format phi
   3.168      |> enclose "(" ")"
   3.169 -  | tptp_string_for_formula format
   3.170 +  | tptp_string_of_formula format
   3.171          (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
   3.172      space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
   3.173 -                  (map (tptp_string_for_term format) ts)
   3.174 +                  (map (tptp_string_of_term format) ts)
   3.175      |> is_format_higher_order format ? enclose "(" ")"
   3.176 -  | tptp_string_for_formula format (AConn (c, [phi])) =
   3.177 -    tptp_string_for_connective c ^ " " ^
   3.178 -    (tptp_string_for_formula format phi
   3.179 +  | tptp_string_of_formula format (AConn (c, [phi])) =
   3.180 +    tptp_string_of_connective c ^ " " ^
   3.181 +    (tptp_string_of_formula format phi
   3.182       |> is_format_higher_order format ? enclose "(" ")")
   3.183      |> enclose "(" ")"
   3.184 -  | tptp_string_for_formula format (AConn (c, phis)) =
   3.185 -    space_implode (" " ^ tptp_string_for_connective c ^ " ")
   3.186 -                  (map (tptp_string_for_formula format) phis)
   3.187 +  | tptp_string_of_formula format (AConn (c, phis)) =
   3.188 +    space_implode (" " ^ tptp_string_of_connective c ^ " ")
   3.189 +                  (map (tptp_string_of_formula format) phis)
   3.190      |> enclose "(" ")"
   3.191 -  | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm
   3.192 +  | tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm
   3.193  
   3.194 -fun tptp_string_for_format CNF = tptp_cnf
   3.195 -  | tptp_string_for_format CNF_UEQ = tptp_cnf
   3.196 -  | tptp_string_for_format FOF = tptp_fof
   3.197 -  | tptp_string_for_format (TFF _) = tptp_tff
   3.198 -  | tptp_string_for_format (THF _) = tptp_thf
   3.199 -  | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format"
   3.200 +fun tptp_string_of_format CNF = tptp_cnf
   3.201 +  | tptp_string_of_format CNF_UEQ = tptp_cnf
   3.202 +  | tptp_string_of_format FOF = tptp_fof
   3.203 +  | tptp_string_of_format (TFF _) = tptp_tff
   3.204 +  | tptp_string_of_format (THF _) = tptp_thf
   3.205 +  | tptp_string_of_format (DFG _) = raise Fail "non-TPTP format"
   3.206  
   3.207  val atype_of_types = AType (tptp_type_of_types, [])
   3.208  
   3.209 @@ -487,24 +487,24 @@
   3.210  fun maybe_alt "" = ""
   3.211    | maybe_alt s = " % " ^ s
   3.212  
   3.213 -fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) =
   3.214 -    tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
   3.215 -  | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
   3.216 -    tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
   3.217 -    " : " ^ string_for_type format ty ^ ").\n"
   3.218 -  | tptp_string_for_line format (Formula ((ident, alt), kind, phi, source, _)) =
   3.219 -    tptp_string_for_format format ^ "(" ^ ident ^ ", " ^
   3.220 -    tptp_string_for_role kind ^ "," ^ maybe_alt alt ^
   3.221 -    "\n    (" ^ tptp_string_for_formula format phi ^ ")" ^
   3.222 +fun tptp_string_of_line format (Type_Decl (ident, ty, ary)) =
   3.223 +    tptp_string_of_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
   3.224 +  | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) =
   3.225 +    tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n    " ^ sym ^
   3.226 +    " : " ^ string_of_type format ty ^ ").\n"
   3.227 +  | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) =
   3.228 +    tptp_string_of_format format ^ "(" ^ ident ^ ", " ^
   3.229 +    tptp_string_of_role kind ^ "," ^ maybe_alt alt ^
   3.230 +    "\n    (" ^ tptp_string_of_formula format phi ^ ")" ^
   3.231      (case source of
   3.232 -       SOME tm => ", " ^ tptp_string_for_term format tm
   3.233 +       SOME tm => ", " ^ tptp_string_of_term format tm
   3.234       | NONE => "") ^ ").\n"
   3.235  
   3.236  fun tptp_lines format =
   3.237    maps (fn (_, []) => []
   3.238           | (heading, lines) =>
   3.239             "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" ::
   3.240 -           map (tptp_string_for_line format) lines)
   3.241 +           map (tptp_string_of_line format) lines)
   3.242  
   3.243  fun arity_of_type (APi (tys, ty)) =
   3.244      arity_of_type ty |>> Integer.add (length tys)
   3.245 @@ -516,20 +516,19 @@
   3.246  
   3.247  val dfg_class_inter = space_implode " & "
   3.248  
   3.249 -fun dfg_string_for_term (ATerm ((s, tys), tms)) =
   3.250 +fun dfg_string_of_term (ATerm ((s, tys), tms)) =
   3.251      s ^
   3.252      (if null tys then ""
   3.253 -     else "<" ^ commas (map (string_for_type (DFG Polymorphic)) tys) ^ ">") ^
   3.254 +     else "<" ^ commas (map (string_of_type (DFG Polymorphic)) tys) ^ ">") ^
   3.255      (if null tms then ""
   3.256 -     else "(" ^ commas (map dfg_string_for_term tms) ^ ")")
   3.257 -  | dfg_string_for_term _ = raise Fail "unexpected atom in first-order format"
   3.258 +     else "(" ^ commas (map dfg_string_of_term tms) ^ ")")
   3.259 +  | dfg_string_of_term _ = raise Fail "unexpected atom in first-order format"
   3.260  
   3.261 -fun dfg_string_for_formula poly gen_simp info =
   3.262 +fun dfg_string_of_formula poly gen_simp info =
   3.263    let
   3.264 -    val str_for_typ = string_for_type (DFG poly)
   3.265 -    fun str_for_bound_typ (ty, []) = str_for_typ ty
   3.266 -      | str_for_bound_typ (ty, cls) =
   3.267 -        str_for_typ ty ^ " : " ^ dfg_class_inter cls
   3.268 +    val str_of_typ = string_of_type (DFG poly)
   3.269 +    fun str_of_bound_typ (ty, []) = str_of_typ ty
   3.270 +      | str_of_bound_typ (ty, cls) = str_of_typ ty ^ " : " ^ dfg_class_inter cls
   3.271      fun suffix_tag top_level s =
   3.272        if top_level then
   3.273          case extract_isabelle_status info of
   3.274 @@ -543,42 +542,42 @@
   3.275          | NONE => s
   3.276        else
   3.277          s
   3.278 -    fun str_for_atom top_level (ATerm ((s, tys), tms)) =
   3.279 +    fun str_of_atom top_level (ATerm ((s, tys), tms)) =
   3.280          let
   3.281            val s' =
   3.282              if is_tptp_equal s then "equal" |> suffix_tag top_level
   3.283              else if s = tptp_true then "true"
   3.284              else if s = tptp_false then "false"
   3.285              else s
   3.286 -        in dfg_string_for_term (ATerm ((s', tys), tms)) end
   3.287 -      | str_for_atom _ _ = raise Fail "unexpected atom in first-order format"
   3.288 -    fun str_for_quant AForall = "forall"
   3.289 -      | str_for_quant AExists = "exists"
   3.290 -    fun str_for_conn _ ANot = "not"
   3.291 -      | str_for_conn _ AAnd = "and"
   3.292 -      | str_for_conn _ AOr = "or"
   3.293 -      | str_for_conn _ AImplies = "implies"
   3.294 -      | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
   3.295 -    fun str_for_formula top_level (ATyQuant (q, xs, phi)) =
   3.296 -        str_for_quant q ^ "_sorts([" ^ commas (map str_for_bound_typ xs) ^
   3.297 -        "], " ^ str_for_formula top_level phi ^ ")"
   3.298 -      | str_for_formula top_level (AQuant (q, xs, phi)) =
   3.299 -        str_for_quant q ^ "([" ^
   3.300 -        commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^
   3.301 -        str_for_formula top_level phi ^ ")"
   3.302 -      | str_for_formula top_level (AConn (c, phis)) =
   3.303 -        str_for_conn top_level c ^ "(" ^
   3.304 -        commas (map (str_for_formula false) phis) ^ ")"
   3.305 -      | str_for_formula top_level (AAtom tm) = str_for_atom top_level tm
   3.306 -  in str_for_formula true end
   3.307 +        in dfg_string_of_term (ATerm ((s', tys), tms)) end
   3.308 +      | str_of_atom _ _ = raise Fail "unexpected atom in first-order format"
   3.309 +    fun str_of_quant AForall = "forall"
   3.310 +      | str_of_quant AExists = "exists"
   3.311 +    fun str_of_conn _ ANot = "not"
   3.312 +      | str_of_conn _ AAnd = "and"
   3.313 +      | str_of_conn _ AOr = "or"
   3.314 +      | str_of_conn _ AImplies = "implies"
   3.315 +      | str_of_conn top_level AIff = "equiv" |> suffix_tag top_level
   3.316 +    fun str_of_formula top_level (ATyQuant (q, xs, phi)) =
   3.317 +        str_of_quant q ^ "_sorts([" ^ commas (map str_of_bound_typ xs) ^ "], " ^
   3.318 +        str_of_formula top_level phi ^ ")"
   3.319 +      | str_of_formula top_level (AQuant (q, xs, phi)) =
   3.320 +        str_of_quant q ^ "([" ^
   3.321 +        commas (map (string_of_bound_var (DFG poly)) xs) ^ "], " ^
   3.322 +        str_of_formula top_level phi ^ ")"
   3.323 +      | str_of_formula top_level (AConn (c, phis)) =
   3.324 +        str_of_conn top_level c ^ "(" ^
   3.325 +        commas (map (str_of_formula false) phis) ^ ")"
   3.326 +      | str_of_formula top_level (AAtom tm) = str_of_atom top_level tm
   3.327 +  in str_of_formula true end
   3.328  
   3.329  fun maybe_enclose bef aft "" = "% " ^ bef ^ aft
   3.330    | maybe_enclose bef aft s = bef ^ s ^ aft
   3.331  
   3.332  fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem =
   3.333    let
   3.334 -    val typ = string_for_type (DFG poly)
   3.335 -    val term = dfg_string_for_term
   3.336 +    val typ = string_of_type (DFG poly)
   3.337 +    val term = dfg_string_of_term
   3.338      fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")"
   3.339      fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty))
   3.340      fun ty_ary 0 ty = ty
   3.341 @@ -602,7 +601,7 @@
   3.342      fun formula pred (Formula ((ident, alt), kind, phi, _, info)) =
   3.343          if pred kind then
   3.344            let val rank = extract_isabelle_rank info in
   3.345 -            "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^
   3.346 +            "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^
   3.347              ", " ^ ident ^
   3.348              (if rank = default_rank then "" else ", " ^ string_of_int rank) ^
   3.349              ")." ^ maybe_alt alt
   3.350 @@ -684,7 +683,7 @@
   3.351      ["end_problem.\n"]
   3.352    end
   3.353  
   3.354 -fun lines_for_atp_problem format ord ord_info problem =
   3.355 +fun lines_of_atp_problem format ord ord_info problem =
   3.356    "% This file was generated by Isabelle (most likely Sledgehammer)\n\
   3.357    \% " ^ timestamp () ^ "\n" ::
   3.358    (case format of
     4.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 15 17:27:24 2013 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 15 17:43:42 2013 +0200
     4.3 @@ -918,7 +918,7 @@
     4.4  fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
     4.5    | ho_term_from_ho_type _ = raise Fail "unexpected type"
     4.6  
     4.7 -fun ho_type_for_type_arg type_enc T =
     4.8 +fun ho_type_of_type_arg type_enc T =
     4.9    if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T)
    4.10  
    4.11  (* This shouldn't clash with anything else. *)
    4.12 @@ -982,7 +982,7 @@
    4.13      (map (native_ho_type_from_typ type_enc false 0) T_args, [])
    4.14    else
    4.15      ([], map_filter (Option.map ho_term_from_ho_type
    4.16 -                     o ho_type_for_type_arg type_enc) T_args)
    4.17 +                     o ho_type_of_type_arg type_enc) T_args)
    4.18  
    4.19  fun class_atom type_enc (cl, T) =
    4.20    let
    4.21 @@ -999,7 +999,7 @@
    4.22  fun class_atoms type_enc (cls, T) =
    4.23    map (fn cl => class_atom type_enc (cl, T)) cls
    4.24  
    4.25 -fun class_membs_for_types type_enc add_sorts_on_typ Ts =
    4.26 +fun class_membs_of_types type_enc add_sorts_on_typ Ts =
    4.27    [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso
    4.28           level_of_type_enc type_enc <> No_Types)
    4.29          ? fold add_sorts_on_typ Ts
    4.30 @@ -1065,7 +1065,7 @@
    4.31                 ty_args ""
    4.32    in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
    4.33  fun mangled_const_name type_enc =
    4.34 -  map_filter (ho_type_for_type_arg type_enc)
    4.35 +  map_filter (ho_type_of_type_arg type_enc)
    4.36    #> raw_mangled_const_name generic_mangled_type_name
    4.37  
    4.38  val parse_mangled_ident =
    4.39 @@ -1579,7 +1579,7 @@
    4.40        end
    4.41    in add_iterm_syms end
    4.42  
    4.43 -fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
    4.44 +fun sym_table_of_facts ctxt type_enc app_op_level conjs facts =
    4.45    let
    4.46      fun add_iterm_syms conj_fact =
    4.47        add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
    4.48 @@ -1773,7 +1773,7 @@
    4.49    case filter is_TVar Ts of
    4.50      [] => I
    4.51    | Ts =>
    4.52 -    (sorts ? mk_ahorn (Ts |> class_membs_for_types type_enc add_sorts_on_tvar
    4.53 +    (sorts ? mk_ahorn (Ts |> class_membs_of_types type_enc add_sorts_on_tvar
    4.54                            |> map (class_atom type_enc)))
    4.55      #> (case type_enc of
    4.56            Native (_, poly, _) =>
    4.57 @@ -1809,8 +1809,8 @@
    4.58    could_specialize_helpers type_enc andalso
    4.59    not (null (Term.hidden_polymorphism t))
    4.60  
    4.61 -fun add_helper_facts_for_sym ctxt format type_enc completish
    4.62 -                             (s, {types, ...} : sym_info) =
    4.63 +fun add_helper_facts_of_sym ctxt format type_enc completish
    4.64 +                            (s, {types, ...} : sym_info) =
    4.65    case unprefix_and_unascii const_prefix s of
    4.66      SOME mangled_s =>
    4.67      let
    4.68 @@ -1852,8 +1852,8 @@
    4.69             (if completish then completish_helper_table else helper_table)
    4.70      end
    4.71    | NONE => I
    4.72 -fun helper_facts_for_sym_table ctxt format type_enc completish sym_tab =
    4.73 -  Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc completish)
    4.74 +fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
    4.75 +  Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish)
    4.76                    sym_tab []
    4.77  
    4.78  (***************************************************************)
    4.79 @@ -2152,7 +2152,7 @@
    4.80  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    4.81     of monomorphization). The TPTP explicitly forbids name clashes, and some of
    4.82     the remote provers might care. *)
    4.83 -fun line_for_fact ctxt prefix encode alt freshen pos mono type_enc rank
    4.84 +fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank
    4.85          (j, {name, stature = (_, status), role, iformula, atomic_types}) =
    4.86    Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
    4.87              encode name, alt name),
    4.88 @@ -2164,21 +2164,21 @@
    4.89             |> bound_tvars type_enc true atomic_types,
    4.90             NONE, isabelle_info (string_of_status status) (rank j))
    4.91  
    4.92 -fun lines_for_subclass type_enc sub super =
    4.93 +fun lines_of_subclass type_enc sub super =
    4.94    Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom,
    4.95             AConn (AImplies,
    4.96                    [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
    4.97             |> bound_tvars type_enc false [tvar_a],
    4.98             NONE, isabelle_info inductiveN helper_rank)
    4.99  
   4.100 -fun lines_for_subclass_pair type_enc (sub, supers) =
   4.101 +fun lines_of_subclass_pair type_enc (sub, supers) =
   4.102    if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
   4.103      [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
   4.104                   map (`make_class) supers)]
   4.105    else
   4.106 -    map (lines_for_subclass type_enc sub) supers
   4.107 +    map (lines_of_subclass type_enc sub) supers
   4.108  
   4.109 -fun line_for_tcon_clause type_enc (name, prems, (cl, T)) =
   4.110 +fun line_of_tcon_clause type_enc (name, prems, (cl, T)) =
   4.111    if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
   4.112      Class_Memb (class_memb_prefix ^ name,
   4.113                  map (fn (cls, T) =>
   4.114 @@ -2192,8 +2192,8 @@
   4.115               |> bound_tvars type_enc true (snd (dest_Type T)),
   4.116               NONE, isabelle_info inductiveN helper_rank)
   4.117  
   4.118 -fun line_for_conjecture ctxt mono type_enc
   4.119 -                        ({name, role, iformula, atomic_types, ...} : ifact) =
   4.120 +fun line_of_conjecture ctxt mono type_enc
   4.121 +                       ({name, role, iformula, atomic_types, ...} : ifact) =
   4.122    Formula ((conjecture_prefix ^ name, ""), role,
   4.123             iformula
   4.124             |> formula_from_iformula ctxt mono type_enc
   4.125 @@ -2201,7 +2201,7 @@
   4.126             |> close_formula_universally
   4.127             |> bound_tvars type_enc true atomic_types, NONE, [])
   4.128  
   4.129 -fun lines_for_free_types type_enc (facts : ifact list) =
   4.130 +fun lines_of_free_types type_enc (facts : ifact list) =
   4.131    if is_type_enc_polymorphic type_enc then
   4.132      let
   4.133        val type_classes =
   4.134 @@ -2216,14 +2216,14 @@
   4.135                     class_atom type_enc (cl, T), NONE, [])
   4.136        val membs =
   4.137          fold (union (op =)) (map #atomic_types facts) []
   4.138 -        |> class_membs_for_types type_enc add_sorts_on_tfree
   4.139 +        |> class_membs_of_types type_enc add_sorts_on_tfree
   4.140      in map2 line (0 upto length membs - 1) membs end
   4.141    else
   4.142      []
   4.143  
   4.144  (** Symbol declarations **)
   4.145  
   4.146 -fun decl_line_for_class phantoms s =
   4.147 +fun decl_line_of_class phantoms s =
   4.148    let val name as (s, _) = `make_class s in
   4.149      Sym_Decl (sym_decl_prefix ^ s, name,
   4.150                APi ([tvar_a_name],
   4.151 @@ -2233,13 +2233,13 @@
   4.152                       bool_atype))
   4.153    end
   4.154  
   4.155 -fun decl_lines_for_classes type_enc classes =
   4.156 +fun decl_lines_of_classes type_enc =
   4.157    case type_enc of
   4.158      Native (_, Raw_Polymorphic phantoms, _) =>
   4.159 -    map (decl_line_for_class phantoms) classes
   4.160 -  | _ => []
   4.161 +    map (decl_line_of_class phantoms)
   4.162 +  | _ => K []
   4.163  
   4.164 -fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
   4.165 +fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) =
   4.166    let
   4.167      fun add_iterm_syms tm =
   4.168        let val (head, args) = strip_iterm_comb tm in
   4.169 @@ -2346,7 +2346,7 @@
   4.170  fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) =
   4.171    formula_fold (SOME (role <> Conjecture))
   4.172                 (add_iterm_mononotonicity_info ctxt level) iformula
   4.173 -fun mononotonicity_info_for_facts ctxt type_enc completish facts =
   4.174 +fun mononotonicity_info_of_facts ctxt type_enc completish facts =
   4.175    let val level = level_of_type_enc type_enc in
   4.176      default_mono level completish
   4.177      |> is_type_level_monotonicity_based level
   4.178 @@ -2367,14 +2367,14 @@
   4.179  fun add_fact_monotonic_types ctxt mono type_enc =
   4.180    ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
   4.181  
   4.182 -fun monotonic_types_for_facts ctxt mono type_enc facts =
   4.183 +fun monotonic_types_of_facts ctxt mono type_enc facts =
   4.184    let val level = level_of_type_enc type_enc in
   4.185      [] |> (is_type_enc_polymorphic type_enc andalso
   4.186             is_type_level_monotonicity_based level)
   4.187            ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
   4.188    end
   4.189  
   4.190 -fun line_for_guards_mono_type ctxt mono type_enc T =
   4.191 +fun line_of_guards_mono_type ctxt mono type_enc T =
   4.192    Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
   4.193             Axiom,
   4.194             IConst (`make_bound_var "X", T, [])
   4.195 @@ -2386,7 +2386,7 @@
   4.196             |> bound_tvars type_enc true (atomic_types_of T),
   4.197             NONE, isabelle_info inductiveN helper_rank)
   4.198  
   4.199 -fun line_for_tags_mono_type ctxt mono type_enc T =
   4.200 +fun line_of_tags_mono_type ctxt mono type_enc T =
   4.201    let val x_var = ATerm ((`make_bound_var "X", []), []) in
   4.202      Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""),
   4.203               Axiom,
   4.204 @@ -2395,14 +2395,13 @@
   4.205               NONE, isabelle_info non_rec_defN helper_rank)
   4.206    end
   4.207  
   4.208 -fun lines_for_mono_types ctxt mono type_enc Ts =
   4.209 +fun lines_of_mono_types ctxt mono type_enc =
   4.210    case type_enc of
   4.211 -    Native _ => []
   4.212 -  | Guards _ => map (line_for_guards_mono_type ctxt mono type_enc) Ts
   4.213 -  | Tags _ => map (line_for_tags_mono_type ctxt mono type_enc) Ts
   4.214 +    Native _ => K []
   4.215 +  | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc)
   4.216 +  | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc)
   4.217  
   4.218 -fun decl_line_for_sym ctxt mono type_enc s
   4.219 -                      (s', T_args, T, pred_sym, ary, _) =
   4.220 +fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) =
   4.221    let
   4.222      val thy = Proof_Context.theory_of ctxt
   4.223      val (T, T_args) =
   4.224 @@ -2425,8 +2424,8 @@
   4.225  
   4.226  fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
   4.227  
   4.228 -fun line_for_guards_sym_decl ctxt mono type_enc n s j
   4.229 -                             (s', T_args, T, _, ary, in_conj) =
   4.230 +fun line_of_guards_sym_decl ctxt mono type_enc n s j
   4.231 +                            (s', T_args, T, _, ary, in_conj) =
   4.232    let
   4.233      val thy = Proof_Context.theory_of ctxt
   4.234      val (role, maybe_negate) = honor_conj_sym_role in_conj
   4.235 @@ -2459,8 +2458,8 @@
   4.236               NONE, isabelle_info inductiveN helper_rank)
   4.237    end
   4.238  
   4.239 -fun lines_for_tags_sym_decl ctxt mono type_enc n s
   4.240 -                            (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   4.241 +fun lines_of_tags_sym_decl ctxt mono type_enc n s
   4.242 +                           (j, (s', T_args, T, pred_sym, ary, in_conj)) =
   4.243    let
   4.244      val thy = Proof_Context.theory_of ctxt
   4.245      val level = level_of_type_enc type_enc
   4.246 @@ -2504,9 +2503,9 @@
   4.247      end
   4.248    | rationalize_decls _ decls = decls
   4.249  
   4.250 -fun lines_for_sym_decls ctxt mono type_enc (s, decls) =
   4.251 +fun lines_of_sym_decls ctxt mono type_enc (s, decls) =
   4.252    case type_enc of
   4.253 -    Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)]
   4.254 +    Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)]
   4.255    | Guards (_, level) =>
   4.256      let
   4.257        val thy = Proof_Context.theory_of ctxt
   4.258 @@ -2517,7 +2516,7 @@
   4.259                           o result_type_of_decl)
   4.260      in
   4.261        (0 upto length decls - 1, decls)
   4.262 -      |-> map2 (line_for_guards_sym_decl ctxt mono type_enc n s)
   4.263 +      |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s)
   4.264      end
   4.265    | Tags (_, level) =>
   4.266      if is_type_level_uniform level then
   4.267 @@ -2525,20 +2524,20 @@
   4.268      else
   4.269        let val n = length decls in
   4.270          (0 upto n - 1 ~~ decls)
   4.271 -        |> maps (lines_for_tags_sym_decl ctxt mono type_enc n s)
   4.272 +        |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s)
   4.273        end
   4.274  
   4.275 -fun lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
   4.276 +fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab =
   4.277    let
   4.278      val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
   4.279 -    val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts
   4.280 -    val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms
   4.281 +    val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts
   4.282 +    val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
   4.283    in mono_lines @ decl_lines end
   4.284  
   4.285  fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2)
   4.286  
   4.287 -fun do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab
   4.288 -                                     base_s0 types in_conj =
   4.289 +fun do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 sym_tab
   4.290 +                                    base_s0 types in_conj =
   4.291    let
   4.292      fun do_alias ary =
   4.293        let
   4.294 @@ -2582,7 +2581,7 @@
   4.295              else pair_append (do_alias (ary - 1)))
   4.296        end
   4.297    in do_alias end
   4.298 -fun uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
   4.299 +fun uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0
   4.300          sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) =
   4.301    case unprefix_and_unascii const_prefix s of
   4.302      SOME mangled_s =>
   4.303 @@ -2590,20 +2589,20 @@
   4.304        let
   4.305          val base_s0 = mangled_s |> unmangled_invert_const
   4.306        in
   4.307 -        do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
   4.308 -                                         sym_tab base_s0 types in_conj min_ary
   4.309 +        do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0
   4.310 +                                        sym_tab base_s0 types in_conj min_ary
   4.311        end
   4.312      else
   4.313        ([], [])
   4.314    | NONE => ([], [])
   4.315 -fun uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
   4.316 -                                        uncurried_aliases sym_tab0 sym_tab =
   4.317 +fun uncurried_alias_lines_of_sym_table ctxt constrs mono type_enc
   4.318 +                                       uncurried_aliases sym_tab0 sym_tab =
   4.319    ([], [])
   4.320    |> uncurried_aliases
   4.321       ? Symtab.fold_rev
   4.322             (pair_append
   4.323 -            o uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0
   4.324 -                                            sym_tab) sym_tab
   4.325 +            o uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0
   4.326 +                                           sym_tab) sym_tab
   4.327  
   4.328  val implicit_declsN = "Should-be-implicit typings"
   4.329  val explicit_declsN = "Explicit typings"
   4.330 @@ -2725,46 +2724,46 @@
   4.331        translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
   4.332                           concl_t facts
   4.333      val (_, sym_tab0) =
   4.334 -      sym_table_for_facts ctxt type_enc app_op_level conjs facts
   4.335 +      sym_table_of_facts ctxt type_enc app_op_level conjs facts
   4.336      val mono =
   4.337 -      conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc completish
   4.338 +      conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish
   4.339      val constrs = all_constrs_of_polymorphic_datatypes thy
   4.340      fun firstorderize in_helper =
   4.341        firstorderize_fact thy constrs type_enc sym_tab0
   4.342            (uncurried_aliases andalso not in_helper) completish
   4.343      val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
   4.344      val (ho_stuff, sym_tab) =
   4.345 -      sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
   4.346 +      sym_table_of_facts ctxt type_enc Min_App_Op conjs facts
   4.347      val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
   4.348 -      uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc
   4.349 -                                          uncurried_aliases sym_tab0 sym_tab
   4.350 +      uncurried_alias_lines_of_sym_table ctxt constrs mono type_enc
   4.351 +                                         uncurried_aliases sym_tab0 sym_tab
   4.352      val (_, sym_tab) =
   4.353        (ho_stuff, sym_tab)
   4.354        |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
   4.355                uncurried_alias_eq_tms
   4.356      val helpers =
   4.357 -      sym_tab |> helper_facts_for_sym_table ctxt format type_enc completish
   4.358 +      sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish
   4.359                |> map (firstorderize true)
   4.360      val mono_Ts =
   4.361 -      helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
   4.362 -    val class_decl_lines = decl_lines_for_classes type_enc classes
   4.363 +      helpers @ conjs @ facts |> monotonic_types_of_facts ctxt mono type_enc
   4.364 +    val class_decl_lines = decl_lines_of_classes type_enc classes
   4.365      val sym_decl_lines =
   4.366        (conjs, helpers @ facts, uncurried_alias_eq_tms)
   4.367 -      |> sym_decl_table_for_facts thy type_enc sym_tab
   4.368 -      |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts
   4.369 +      |> sym_decl_table_of_facts thy type_enc sym_tab
   4.370 +      |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts
   4.371      val num_facts = length facts
   4.372      val fact_lines =
   4.373 -      map (line_for_fact ctxt fact_prefix ascii_of I (not exporter)
   4.374 +      map (line_of_fact ctxt fact_prefix ascii_of I (not exporter)
   4.375                 (not exporter) mono type_enc (rank_of_fact_num num_facts))
   4.376            (0 upto num_facts - 1 ~~ facts)
   4.377 -    val subclass_lines = maps (lines_for_subclass_pair type_enc) subclass_pairs
   4.378 -    val tcon_lines = map (line_for_tcon_clause type_enc) tcon_clauses
   4.379 +    val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs
   4.380 +    val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses
   4.381      val helper_lines =
   4.382        0 upto length helpers - 1 ~~ helpers
   4.383 -      |> map (line_for_fact ctxt helper_prefix I (K "") false true mono type_enc
   4.384 -                            (K default_rank))
   4.385 -    val free_type_lines = lines_for_free_types type_enc (facts @ conjs)
   4.386 -    val conj_lines = map (line_for_conjecture ctxt mono type_enc) conjs
   4.387 +      |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc
   4.388 +                           (K default_rank))
   4.389 +    val free_type_lines = lines_of_free_types type_enc (facts @ conjs)
   4.390 +    val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs
   4.391      (* Reordering these might confuse the proof reconstruction code. *)
   4.392      val problem =
   4.393        [(explicit_declsN, class_decl_lines @ sym_decl_lines),
     5.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed May 15 17:27:24 2013 +0200
     5.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed May 15 17:43:42 2013 +0200
     5.3 @@ -41,7 +41,7 @@
     5.4    type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
     5.5  
     5.6    val short_output : bool -> string -> string
     5.7 -  val string_for_failure : failure -> string
     5.8 +  val string_of_failure : failure -> string
     5.9    val extract_important_message : string -> string
    5.10    val extract_known_failure :
    5.11      (failure * string) list -> string -> failure option
    5.12 @@ -105,27 +105,27 @@
    5.13      "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
    5.14      " "
    5.15  
    5.16 -fun string_for_failure Unprovable = "The generated problem is unprovable."
    5.17 -  | string_for_failure GaveUp = "The prover gave up."
    5.18 -  | string_for_failure ProofMissing =
    5.19 +fun string_of_failure Unprovable = "The generated problem is unprovable."
    5.20 +  | string_of_failure GaveUp = "The prover gave up."
    5.21 +  | string_of_failure ProofMissing =
    5.22      "The prover claims the conjecture is a theorem but did not provide a proof."
    5.23 -  | string_for_failure ProofIncomplete =
    5.24 +  | string_of_failure ProofIncomplete =
    5.25      "The prover claims the conjecture is a theorem but provided an incomplete \
    5.26      \(or unparsable) proof."
    5.27 -  | string_for_failure (UnsoundProof (false, ss)) =
    5.28 +  | string_of_failure (UnsoundProof (false, ss)) =
    5.29      "The prover found an unsound proof " ^ involving ss ^
    5.30      "(or, less likely, your axioms are inconsistent). Specify a sound type \
    5.31      \encoding or omit the \"type_enc\" option."
    5.32 -  | string_for_failure (UnsoundProof (true, ss)) =
    5.33 +  | string_of_failure (UnsoundProof (true, ss)) =
    5.34      "The prover found an unsound proof " ^ involving ss ^
    5.35      "(or, less likely, your axioms are inconsistent). Please report this to \
    5.36      \the Isabelle developers."
    5.37 -  | string_for_failure CantConnect = "Cannot connect to remote server."
    5.38 -  | string_for_failure TimedOut = "Timed out."
    5.39 -  | string_for_failure Inappropriate =
    5.40 +  | string_of_failure CantConnect = "Cannot connect to remote server."
    5.41 +  | string_of_failure TimedOut = "Timed out."
    5.42 +  | string_of_failure Inappropriate =
    5.43      "The generated problem lies outside the prover's scope."
    5.44 -  | string_for_failure OutOfResources = "The prover ran out of resources."
    5.45 -  | string_for_failure OldSPASS =
    5.46 +  | string_of_failure OutOfResources = "The prover ran out of resources."
    5.47 +  | string_of_failure OldSPASS =
    5.48      "The version of SPASS you are using is obsolete. Please upgrade to \
    5.49      \SPASS 3.8ds. To install it, download and extract the package \
    5.50      \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
    5.51 @@ -134,20 +134,20 @@
    5.52                 (Path.variable "ISABELLE_HOME_USER" ::
    5.53                  map Path.basic ["etc", "components"])))) ^
    5.54      " on a line of its own."
    5.55 -  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
    5.56 -  | string_for_failure NoLibwwwPerl =
    5.57 +  | string_of_failure NoPerl = "Perl" ^ missing_message_tail
    5.58 +  | string_of_failure NoLibwwwPerl =
    5.59      "The Perl module \"libwww-perl\"" ^ missing_message_tail
    5.60 -  | string_for_failure MalformedInput =
    5.61 +  | string_of_failure MalformedInput =
    5.62      "The generated problem is malformed. Please report this to the Isabelle \
    5.63      \developers."
    5.64 -  | string_for_failure MalformedOutput = "The prover output is malformed."
    5.65 -  | string_for_failure Interrupted = "The prover was interrupted."
    5.66 -  | string_for_failure Crashed = "The prover crashed."
    5.67 -  | string_for_failure InternalError = "An internal prover error occurred."
    5.68 -  | string_for_failure (UnknownError string) =
    5.69 +  | string_of_failure MalformedOutput = "The prover output is malformed."
    5.70 +  | string_of_failure Interrupted = "The prover was interrupted."
    5.71 +  | string_of_failure Crashed = "The prover crashed."
    5.72 +  | string_of_failure InternalError = "An internal prover error occurred."
    5.73 +  | string_of_failure (UnknownError s) =
    5.74      "A prover error occurred" ^
    5.75 -    (if string = "" then ". (Pass the \"verbose\" option for details.)"
    5.76 -     else ":\n" ^ string)
    5.77 +    (if s = "" then ". (Pass the \"verbose\" option for details.)"
    5.78 +     else ":\n" ^ s)
    5.79  
    5.80  fun extract_delimited (begin_delim, end_delim) output =
    5.81    output |> first_field begin_delim |> the |> snd
     6.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Wed May 15 17:27:24 2013 +0200
     6.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed May 15 17:43:42 2013 +0200
     6.3 @@ -646,7 +646,7 @@
     6.4            (output, 0) => split_lines output
     6.5          | (output, _) =>
     6.6            (warning (case extract_known_failure known_perl_failures output of
     6.7 -                      SOME failure => string_for_failure failure
     6.8 +                      SOME failure => string_of_failure failure
     6.9                      | NONE => trim_line output ^ "."); [])) ()
    6.10    handle TimeLimit.TimeOut => []
    6.11  
     7.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Wed May 15 17:27:24 2013 +0200
     7.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Wed May 15 17:43:42 2013 +0200
     7.3 @@ -246,7 +246,7 @@
     7.4                            false false [] @{prop False} props
     7.5      (*
     7.6      val _ = tracing ("ATP PROBLEM: " ^
     7.7 -                     cat_lines (lines_for_atp_problem CNF atp_problem))
     7.8 +                     cat_lines (lines_of_atp_problem CNF atp_problem))
     7.9      *)
    7.10      (* "rev" is for compatibility with existing proof scripts. *)
    7.11      val axioms =
     8.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 15 17:27:24 2013 +0200
     8.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 15 17:43:42 2013 +0200
     8.3 @@ -656,7 +656,7 @@
     8.4                           #> pairself (Envir.subst_term_types tyenv))
     8.5            val tysubst = tyenv |> Vartab.dest
     8.6          in (tysubst, tsubst) end
     8.7 -      fun subst_info_for_prem subgoal_no prem =
     8.8 +      fun subst_info_of_prem subgoal_no prem =
     8.9          case prem of
    8.10            _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
    8.11            let val ax_no = HOLogic.dest_nat num in
    8.12 @@ -675,7 +675,7 @@
    8.13              NONE
    8.14        fun clusters_in_term skolem t =
    8.15          Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
    8.16 -      fun deps_for_term_subst (var, t) =
    8.17 +      fun deps_of_term_subst (var, t) =
    8.18          case clusters_in_term false var of
    8.19            [] => NONE
    8.20          | [(ax_no, cluster_no)] =>
    8.21 @@ -684,9 +684,9 @@
    8.22                  |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
    8.23          | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
    8.24        val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
    8.25 -      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
    8.26 +      val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
    8.27                           |> sort (int_ord o pairself fst)
    8.28 -      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
    8.29 +      val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
    8.30        val clusters = maps (op ::) depss
    8.31        val ordered_clusters =
    8.32          Int_Pair_Graph.empty
    8.33 @@ -720,7 +720,7 @@
    8.34                           cluster_no = 0 andalso skolem)
    8.35             |> sort shuffle_ord |> map (fst o snd)
    8.36  (* for debugging only:
    8.37 -      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
    8.38 +      fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
    8.39          "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
    8.40          "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
    8.41          commas (map ((fn (s, t) => s ^ " |-> " ^ t)
    8.42 @@ -729,12 +729,12 @@
    8.43        val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
    8.44        val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
    8.45        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    8.46 -                       cat_lines (map string_for_subst_info substs))
    8.47 +                       cat_lines (map string_of_subst_info substs))
    8.48  *)
    8.49        fun cut_and_ex_tac axiom =
    8.50          cut_tac axiom 1
    8.51          THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
    8.52 -      fun rotation_for_subgoal i =
    8.53 +      fun rotation_of_subgoal i =
    8.54          find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
    8.55      in
    8.56        Goal.prove ctxt [] [] @{prop False}
    8.57 @@ -746,7 +746,7 @@
    8.58                THEN match_tac [prems_imp_false] 1
    8.59                THEN ALLGOALS (fn i =>
    8.60                         rtac @{thm Meson.skolem_COMBK_I} i
    8.61 -                       THEN rotate_tac (rotation_for_subgoal i) i
    8.62 +                       THEN rotate_tac (rotation_of_subgoal i) i
    8.63                         THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    8.64                         THEN assume_tac i
    8.65                         THEN flexflex_tac)))
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed May 15 17:27:24 2013 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed May 15 17:43:42 2013 +0200
     9.3 @@ -216,7 +216,7 @@
     9.4          (* TODO: add Skolem variables to context? *)
     9.5          fun enrich_with_fact l t =
     9.6            Proof_Context.put_thms false
     9.7 -            (string_for_label l, SOME [Skip_Proof.make_thm thy t])
     9.8 +              (string_of_label l, SOME [Skip_Proof.make_thm thy t])
     9.9          fun enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t
    9.10            | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t
    9.11            | enrich_with_step _ = I
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 15 17:27:24 2013 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed May 15 17:43:42 2013 +0200
    10.3 @@ -245,7 +245,7 @@
    10.4    (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
    10.5    exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
    10.6  
    10.7 -fun hackish_string_for_term ctxt =
    10.8 +fun hackish_string_of_term ctxt =
    10.9    with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
   10.10  
   10.11  (* This is a terrible hack. Free variables are sometimes coded as "M__" when
   10.12 @@ -269,12 +269,8 @@
   10.13            (Term.add_vars t [] |> sort_wrt (fst o fst))
   10.14    |> fst
   10.15  
   10.16 -fun backquote_term ctxt t =
   10.17 -  t |> close_form
   10.18 -    |> hackish_string_for_term ctxt
   10.19 -    |> backquote
   10.20 -
   10.21 -fun backquote_thm ctxt th = backquote_term ctxt (prop_of th)
   10.22 +fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote
   10.23 +fun backquote_thm ctxt = backquote_term ctxt o prop_of
   10.24  
   10.25  fun clasimpset_rule_table_of ctxt =
   10.26    let
   10.27 @@ -384,7 +380,7 @@
   10.28      val p_inst =
   10.29        concl_prop |> map_aterms varify_noninducts |> close_form
   10.30                   |> lambda (Free ind_x)
   10.31 -                 |> hackish_string_for_term ctxt
   10.32 +                 |> hackish_string_of_term ctxt
   10.33    in
   10.34      ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
   10.35        stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 17:27:24 2013 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed May 15 17:43:42 2013 +0200
    11.3 @@ -334,13 +334,13 @@
    11.4  
    11.5  fun is_raw_param_relevant_for_minimize (name, _) =
    11.6    member (op =) params_for_minimize name
    11.7 -fun string_for_raw_param (key, values) =
    11.8 +fun string_of_raw_param (key, values) =
    11.9    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
   11.10 -fun nice_string_for_raw_param (p as (key, ["false"])) =
   11.11 +fun nice_string_of_raw_param (p as (key, ["false"])) =
   11.12      (case AList.find (op =) negated_alias_params key of
   11.13         [neg] => neg
   11.14 -     | _ => string_for_raw_param p)
   11.15 -  | nice_string_for_raw_param p = string_for_raw_param p
   11.16 +     | _ => string_of_raw_param p)
   11.17 +  | nice_string_of_raw_param p = string_of_raw_param p
   11.18  
   11.19  fun minimize_command override_params i more_override_params prover_name
   11.20                       fact_names =
   11.21 @@ -350,7 +350,7 @@
   11.22         |> filter_out (AList.defined (op =) more_override_params o fst)) @
   11.23        more_override_params
   11.24        |> filter is_raw_param_relevant_for_minimize
   11.25 -      |> map nice_string_for_raw_param
   11.26 +      |> map nice_string_of_raw_param
   11.27        |> (if prover_name = default_minimize_prover then I else cons prover_name)
   11.28        |> space_implode ", "
   11.29    in
   11.30 @@ -428,7 +428,7 @@
   11.31    Toplevel.keep (hammer_away params subcommand opt_i fact_override
   11.32                   o Toplevel.proof_of)
   11.33  
   11.34 -fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
   11.35 +fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value
   11.36  
   11.37  fun sledgehammer_params_trans params =
   11.38    Toplevel.theory
   11.39 @@ -439,7 +439,7 @@
   11.40                               (case default_raw_params ctxt |> rev of
   11.41                                  [] => "none"
   11.42                                | params =>
   11.43 -                                params |> map string_for_raw_param
   11.44 +                                params |> map string_of_raw_param
   11.45                                         |> sort_strings |> cat_lines))
   11.46                    end))
   11.47  
    12.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 15 17:27:24 2013 +0200
    12.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 15 17:43:42 2013 +0200
    12.3 @@ -574,7 +574,7 @@
    12.4      val thy = Proof_Context.theory_of ctxt
    12.5      fun is_built_in (x as (s, _)) args =
    12.6        if member (op =) logical_consts s then (true, args)
    12.7 -      else is_built_in_const_for_prover ctxt prover x args
    12.8 +      else is_built_in_const_of_prover ctxt prover x args
    12.9      val fixes = map snd (Variable.dest_fixes ctxt)
   12.10      val classes = Sign.classes_of thy
   12.11      fun add_classes @{sort type} = I
    13.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed May 15 17:27:24 2013 +0200
    13.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed May 15 17:43:42 2013 +0200
    13.3 @@ -50,11 +50,11 @@
    13.4  datatype pattern = PVar | PApp of string * pattern list
    13.5  datatype ptype = PType of int * pattern list
    13.6  
    13.7 -fun string_for_pattern PVar = "_"
    13.8 -  | string_for_pattern (PApp (s, ps)) =
    13.9 -    if null ps then s else s ^ string_for_patterns ps
   13.10 -and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
   13.11 -fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
   13.12 +fun string_of_pattern PVar = "_"
   13.13 +  | string_of_pattern (PApp (s, ps)) =
   13.14 +    if null ps then s else s ^ string_of_patterns ps
   13.15 +and string_of_patterns ps = "(" ^ commas (map string_of_pattern ps) ^ ")"
   13.16 +fun string_of_ptype (PType (_, ps)) = string_of_patterns ps
   13.17  
   13.18  (*Is the second type an instance of the first one?*)
   13.19  fun match_pattern (PVar, _) = true
   13.20 @@ -74,20 +74,20 @@
   13.21  fun pconst_hyper_mem f const_tab (s, ps) =
   13.22    exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
   13.23  
   13.24 -fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
   13.25 -  | pattern_for_type (TFree (s, _)) = PApp (s, [])
   13.26 -  | pattern_for_type (TVar _) = PVar
   13.27 +fun pattern_of_type (Type (s, Ts)) = PApp (s, map pattern_of_type Ts)
   13.28 +  | pattern_of_type (TFree (s, _)) = PApp (s, [])
   13.29 +  | pattern_of_type (TVar _) = PVar
   13.30  
   13.31  (* Pairs a constant with the list of its type instantiations. *)
   13.32  fun ptype thy const x =
   13.33 -  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
   13.34 +  (if const then map pattern_of_type (these (try (Sign.const_typargs thy) x))
   13.35     else [])
   13.36  fun rich_ptype thy const (s, T) =
   13.37    PType (order_of_type T, ptype thy const (s, T))
   13.38  fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
   13.39  
   13.40 -fun string_for_hyper_pconst (s, ps) =
   13.41 -  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
   13.42 +fun string_of_hyper_pconst (s, ps) =
   13.43 +  s ^ "{" ^ commas (map string_of_ptype ps) ^ "}"
   13.44  
   13.45  (* Add a pconstant to the table, but a [] entry means a standard
   13.46     connective, which we ignore.*)
   13.47 @@ -264,7 +264,7 @@
   13.48      * pow_int higher_order_irrel_weight (order - 1)
   13.49    end
   13.50  
   13.51 -fun multiplier_for_const_name local_const_multiplier s =
   13.52 +fun multiplier_of_const_name local_const_multiplier s =
   13.53    if String.isSubstring "." s then 1.0 else local_const_multiplier
   13.54  
   13.55  (* Computes a constant's weight, as determined by its frequency. *)
   13.56 @@ -278,7 +278,7 @@
   13.57    else if String.isSuffix theory_const_suffix s then
   13.58      theory_const_weight
   13.59    else
   13.60 -    multiplier_for_const_name local_const_multiplier s
   13.61 +    multiplier_of_const_name local_const_multiplier s
   13.62      * weight_for m (pconst_freq (match_ptype o f) const_tab c)
   13.63      |> (if chained_const_weight < 1.0 andalso
   13.64             pconst_hyper_mem I chained_const_tab c then
   13.65 @@ -448,7 +448,7 @@
   13.66                trace_msg ctxt (fn () => "New or updated constants: " ^
   13.67                    commas (rel_const_tab' |> Symtab.dest
   13.68                            |> subtract (op =) (rel_const_tab |> Symtab.dest)
   13.69 -                          |> map string_for_hyper_pconst));
   13.70 +                          |> map string_of_hyper_pconst));
   13.71                map (fst o fst) accepts @
   13.72                (if remaining_max = 0 then
   13.73                   []
   13.74 @@ -477,7 +477,7 @@
   13.75                Real.toString thres ^ ", constants: " ^
   13.76                commas (rel_const_tab |> Symtab.dest
   13.77                        |> filter (curry (op <>) [] o snd)
   13.78 -                      |> map string_for_hyper_pconst));
   13.79 +                      |> map string_of_hyper_pconst));
   13.80            relevant [] [] hopeful
   13.81          end
   13.82      fun uses_const s t =
   13.83 @@ -516,11 +516,11 @@
   13.84    let
   13.85      val thy = Proof_Context.theory_of ctxt
   13.86      val is_built_in_const =
   13.87 -      Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover
   13.88 +      Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover
   13.89      val fudge =
   13.90        case fudge of
   13.91          SOME fudge => fudge
   13.92 -      | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover
   13.93 +      | NONE => Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover
   13.94      val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0),
   13.95                            1.0 / Real.fromInt (max_facts + 1))
   13.96    in
    14.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed May 15 17:27:24 2013 +0200
    14.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed May 15 17:43:42 2013 +0200
    14.3 @@ -91,7 +91,7 @@
    14.4      print silent
    14.5            (fn () =>
    14.6                case outcome of
    14.7 -                SOME failure => string_for_failure failure
    14.8 +                SOME failure => string_of_failure failure
    14.9                | NONE =>
   14.10                  "Found proof" ^
   14.11                   (if length used_facts = length facts then ""
    15.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed May 15 17:27:24 2013 +0200
    15.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed May 15 17:43:42 2013 +0200
    15.3 @@ -69,7 +69,7 @@
    15.4  (* lookup facts in context *)
    15.5  fun resolve_fact_names ctxt names =
    15.6    (names
    15.7 -    |>> map string_for_label
    15.8 +    |>> map string_of_label
    15.9      |> op @
   15.10      |> maps (thms_of_name ctxt))
   15.11    handle ERROR msg => error ("preplay error: " ^ msg)
    16.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 15 17:27:24 2013 +0200
    16.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed May 15 17:43:42 2013 +0200
    16.3 @@ -28,7 +28,7 @@
    16.4    val no_label : label
    16.5    val no_facts : facts
    16.6  
    16.7 -  val string_for_label : label -> string
    16.8 +  val string_of_label : label -> string
    16.9    val fix_of_proof : isar_proof -> fix
   16.10    val assms_of_proof : isar_proof -> assms
   16.11    val steps_of_proof : isar_proof -> isar_step list
   16.12 @@ -63,7 +63,7 @@
   16.13  val no_label = ("", ~1)
   16.14  val no_facts = ([],[])
   16.15  
   16.16 -fun string_for_label (s, num) = s ^ string_of_int num
   16.17 +fun string_of_label (s, num) = s ^ string_of_int num
   16.18  
   16.19  fun fix_of_proof (Proof (fix, _, _)) = fix
   16.20  fun assms_of_proof (Proof (_, assms, _)) = assms
    17.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 15 17:27:24 2013 +0200
    17.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 15 17:43:42 2013 +0200
    17.3 @@ -115,14 +115,14 @@
    17.4      Proof.context -> string -> string option
    17.5    val remotify_prover_if_not_installed :
    17.6      Proof.context -> string -> string option
    17.7 -  val default_max_facts_for_prover : Proof.context -> bool -> string -> int
    17.8 +  val default_max_facts_of_prover : Proof.context -> bool -> string -> int
    17.9    val is_unit_equality : term -> bool
   17.10 -  val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
   17.11 -  val is_built_in_const_for_prover :
   17.12 +  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
   17.13 +  val is_built_in_const_of_prover :
   17.14      Proof.context -> string -> string * typ -> term list -> bool * term list
   17.15    val atp_relevance_fudge : relevance_fudge
   17.16    val smt_relevance_fudge : relevance_fudge
   17.17 -  val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge
   17.18 +  val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge
   17.19    val weight_smt_fact :
   17.20      Proof.context -> int -> ((string * stature) * thm) * int
   17.21      -> (string * stature) * (int option * thm)
   17.22 @@ -171,7 +171,7 @@
   17.23  
   17.24  fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt)
   17.25  
   17.26 -fun is_atp_for_format is_format ctxt name =
   17.27 +fun is_atp_of_format is_format ctxt name =
   17.28    let val thy = Proof_Context.theory_of ctxt in
   17.29      case try (get_atp thy) name of
   17.30        SOME config =>
   17.31 @@ -180,8 +180,8 @@
   17.32      | NONE => false
   17.33    end
   17.34  
   17.35 -val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ)
   17.36 -val is_ho_atp = is_atp_for_format is_format_higher_order
   17.37 +val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
   17.38 +val is_ho_atp = is_atp_of_format is_format_higher_order
   17.39  
   17.40  fun is_prover_supported ctxt =
   17.41    let val thy = Proof_Context.theory_of ctxt in
   17.42 @@ -213,7 +213,7 @@
   17.43  
   17.44  fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts
   17.45  
   17.46 -fun default_max_facts_for_prover ctxt slice name =
   17.47 +fun default_max_facts_of_prover ctxt slice name =
   17.48    let val thy = Proof_Context.theory_of ctxt in
   17.49      if is_reconstructor name then
   17.50        reconstructor_default_max_facts
   17.51 @@ -243,10 +243,10 @@
   17.52      is_good_unit_equality T t u
   17.53    | is_unit_equality _ = false
   17.54  
   17.55 -fun is_appropriate_prop_for_prover ctxt name =
   17.56 +fun is_appropriate_prop_of_prover ctxt name =
   17.57    if is_unit_equational_atp ctxt name then is_unit_equality else K true
   17.58  
   17.59 -fun is_built_in_const_for_prover ctxt name =
   17.60 +fun is_built_in_const_of_prover ctxt name =
   17.61    if is_smt_prover ctxt name then
   17.62      let val ctxt = ctxt |> select_smt_solver name in
   17.63        fn x => fn ts =>
   17.64 @@ -304,7 +304,7 @@
   17.65     threshold_divisor = #threshold_divisor atp_relevance_fudge,
   17.66     ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge}
   17.67  
   17.68 -fun relevance_fudge_for_prover ctxt name =
   17.69 +fun relevance_fudge_of_prover ctxt name =
   17.70    if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge
   17.71  
   17.72  fun supported_provers ctxt =
   17.73 @@ -445,7 +445,7 @@
   17.74      (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
   17.75    end
   17.76  
   17.77 -fun overlord_file_location_for_prover prover =
   17.78 +fun overlord_file_location_of_prover prover =
   17.79    (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
   17.80  
   17.81  fun proof_banner mode name =
   17.82 @@ -490,14 +490,14 @@
   17.83      val full_tac = Method.insert_tac facts i THEN tac ctxt i
   17.84    in time_limit timeout (try (Seq.pull o full_tac)) goal end
   17.85  
   17.86 -fun tac_for_reconstructor (Metis (type_enc, lam_trans)) =
   17.87 +fun tac_of_reconstructor (Metis (type_enc, lam_trans)) =
   17.88      metis_tac [type_enc] lam_trans
   17.89 -  | tac_for_reconstructor SMT = SMT_Solver.smt_tac
   17.90 +  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
   17.91  
   17.92  fun timed_reconstructor reconstr debug timeout ths =
   17.93    (Config.put Metis_Tactic.verbose debug
   17.94     #> Config.put SMT_Config.verbose debug
   17.95 -   #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths))
   17.96 +   #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
   17.97    |> timed_apply timeout
   17.98  
   17.99  fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
  17.100 @@ -528,7 +528,7 @@
  17.101              let
  17.102                val _ =
  17.103                  if verbose then
  17.104 -                  "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^
  17.105 +                  "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
  17.106                    (case timeout of
  17.107                       SOME timeout => " for " ^ string_from_time timeout
  17.108                     | NONE => "") ^ "..."
  17.109 @@ -553,8 +553,8 @@
  17.110     clearly inconsistent facts such as X = a | X = b, though it by no means
  17.111     guarantees soundness. *)
  17.112  
  17.113 -fun get_facts_for_filter _ [(_, facts)] = facts
  17.114 -  | get_facts_for_filter fact_filter factss =
  17.115 +fun get_facts_of_filter _ [(_, facts)] = facts
  17.116 +  | get_facts_of_filter fact_filter factss =
  17.117      case AList.lookup (op =) factss fact_filter of
  17.118        SOME facts => facts
  17.119      | NONE => snd (hd factss)
  17.120 @@ -647,12 +647,12 @@
  17.121           (max_new_instances |> the_default best_max_new_instances)
  17.122    #> Config.put Legacy_Monomorph.keep_partial_instances false
  17.123  
  17.124 -fun suffix_for_mode Auto_Try = "_try"
  17.125 -  | suffix_for_mode Try = "_try"
  17.126 -  | suffix_for_mode Normal = ""
  17.127 -  | suffix_for_mode MaSh = ""
  17.128 -  | suffix_for_mode Auto_Minimize = "_min"
  17.129 -  | suffix_for_mode Minimize = "_min"
  17.130 +fun suffix_of_mode Auto_Try = "_try"
  17.131 +  | suffix_of_mode Try = "_try"
  17.132 +  | suffix_of_mode Normal = ""
  17.133 +  | suffix_of_mode MaSh = ""
  17.134 +  | suffix_of_mode Auto_Minimize = "_min"
  17.135 +  | suffix_of_mode Minimize = "_min"
  17.136  
  17.137  (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on
  17.138     Linux appears to be the only ATP that does not honor its time limit. *)
  17.139 @@ -681,11 +681,11 @@
  17.140        else Sledgehammer
  17.141      val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
  17.142      val (dest_dir, problem_prefix) =
  17.143 -      if overlord then overlord_file_location_for_prover name
  17.144 +      if overlord then overlord_file_location_of_prover name
  17.145        else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)
  17.146      val problem_file_name =
  17.147        Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
  17.148 -                  suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
  17.149 +                  suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
  17.150      val prob_path =
  17.151        if dest_dir = "" then
  17.152          File.tmp_path problem_file_name
  17.153 @@ -763,7 +763,7 @@
  17.154            let
  17.155              val effective_fact_filter =
  17.156                fact_filter |> the_default best_fact_filter
  17.157 -            val facts = get_facts_for_filter effective_fact_filter factss
  17.158 +            val facts = get_facts_of_filter effective_fact_filter factss
  17.159              val num_facts =
  17.160                Real.ceil (max_fact_factor * Real.fromInt best_max_facts) +
  17.161                max_fact_factor_fudge
  17.162 @@ -834,7 +834,7 @@
  17.163                |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
  17.164              val _ =
  17.165                atp_problem
  17.166 -              |> lines_for_atp_problem format ord ord_info
  17.167 +              |> lines_of_atp_problem format ord ord_info
  17.168                |> cons ("% " ^ command ^ "\n")
  17.169                |> File.write_list prob_path
  17.170              val ((output, run_time), used_from, (atp_proof, outcome)) =
  17.171 @@ -864,7 +864,7 @@
  17.172                       val failure =
  17.173                         UnsoundProof (is_type_enc_sound type_enc, facts)
  17.174                     in
  17.175 -                     if debug then (warning (string_for_failure failure); NONE)
  17.176 +                     if debug then (warning (string_of_failure failure); NONE)
  17.177                       else SOME failure
  17.178                     end
  17.179                   | NONE => NONE)
  17.180 @@ -966,7 +966,7 @@
  17.181          end
  17.182        | SOME failure =>
  17.183          ([], Lazy.value (Failed_to_Play plain_metis),
  17.184 -         fn _ => string_for_failure failure, "")
  17.185 +         fn _ => string_of_failure failure, "")
  17.186    in
  17.187      {outcome = outcome, used_facts = used_facts, used_from = used_from,
  17.188       run_time = run_time, preplay = preplay, message = message,
  17.189 @@ -1024,7 +1024,7 @@
  17.190             |> Config.put SMT_Config.verbose debug
  17.191             |> (if overlord then
  17.192                   Config.put SMT_Config.debug_files
  17.193 -                            (overlord_file_location_for_prover name
  17.194 +                            (overlord_file_location_of_prover name
  17.195                               |> (fn (path, name) => path ^ "/" ^ name))
  17.196                 else
  17.197                   I)
  17.198 @@ -1112,7 +1112,7 @@
  17.199                if verbose andalso is_some outcome then
  17.200                  quote name ^ " invoked with " ^
  17.201                  num_of_facts fact_filter num_facts ^ ": " ^
  17.202 -                string_for_failure (failure_from_smt_failure (the outcome)) ^
  17.203 +                string_of_failure (failure_from_smt_failure (the outcome)) ^
  17.204                  " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
  17.205                  "..."
  17.206                  |> Output.urgent_message
  17.207 @@ -1166,7 +1166,7 @@
  17.208             "")
  17.209        | SOME failure =>
  17.210          (Lazy.value (Failed_to_Play plain_metis),
  17.211 -         fn _ => string_for_failure failure, "")
  17.212 +         fn _ => string_of_failure failure, "")
  17.213    in
  17.214      {outcome = outcome, used_facts = used_facts, used_from = used_from,
  17.215       run_time = run_time, preplay = preplay, message = message,
  17.216 @@ -1212,7 +1212,7 @@
  17.217        in
  17.218          {outcome = SOME failure, used_facts = [], used_from = [],
  17.219           run_time = Time.zeroTime, preplay = Lazy.value play,
  17.220 -         message = fn _ => string_for_failure failure, message_tail = ""}
  17.221 +         message = fn _ => string_of_failure failure, message_tail = ""}
  17.222        end
  17.223    end
  17.224  
    18.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed May 15 17:27:24 2013 +0200
    18.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed May 15 17:43:42 2013 +0200
    18.3 @@ -27,7 +27,7 @@
    18.4      * (string * stature) list vector * int Symtab.table * string proof * thm
    18.5  
    18.6    val smtN : string
    18.7 -  val string_for_reconstructor : reconstructor -> string
    18.8 +  val string_of_reconstructor : reconstructor -> string
    18.9    val lam_trans_from_atp_proof : string proof -> string -> string
   18.10    val is_typed_helper_used_in_atp_proof : string proof -> bool
   18.11    val used_facts_in_atp_proof :
   18.12 @@ -78,9 +78,9 @@
   18.13  
   18.14  val smtN = "smt"
   18.15  
   18.16 -fun string_for_reconstructor (Metis (type_enc, lam_trans)) =
   18.17 +fun string_of_reconstructor (Metis (type_enc, lam_trans)) =
   18.18      metis_call type_enc lam_trans
   18.19 -  | string_for_reconstructor SMT = smtN
   18.20 +  | string_of_reconstructor SMT = smtN
   18.21  
   18.22  
   18.23  (** fact extraction from ATP proofs **)
   18.24 @@ -207,7 +207,7 @@
   18.25  
   18.26  fun using_labels [] = ""
   18.27    | using_labels ls =
   18.28 -    "using " ^ space_implode " " (map string_for_label ls) ^ " "
   18.29 +    "using " ^ space_implode " " (map string_of_label ls) ^ " "
   18.30  
   18.31  fun command_call name [] =
   18.32      name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
   18.33 @@ -216,7 +216,7 @@
   18.34  fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
   18.35    (* unusing_chained_facts used_chaineds num_chained ^ *)
   18.36    using_labels ls ^ apply_on_subgoal i n ^
   18.37 -  command_call (string_for_reconstructor reconstr) ss
   18.38 +  command_call (string_of_reconstructor reconstr) ss
   18.39  
   18.40  fun try_command_line banner time command =
   18.41    banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
   18.42 @@ -270,14 +270,14 @@
   18.43  val have_prefix = "f"
   18.44  val raw_prefix = "x"
   18.45  
   18.46 -fun raw_label_for_name (num, ss) =
   18.47 +fun raw_label_of_name (num, ss) =
   18.48    case resolve_conjecture ss of
   18.49      [j] => (conjecture_prefix, j)
   18.50    | _ => (raw_prefix ^ ascii_of num, 0)
   18.51  
   18.52 -fun label_of_clause [name] = raw_label_for_name name
   18.53 +fun label_of_clause [name] = raw_label_of_name name
   18.54    | label_of_clause c =
   18.55 -    (space_implode "___" (map (fst o raw_label_for_name) c), 0)
   18.56 +    (space_implode "___" (map (fst o raw_label_of_name) c), 0)
   18.57  
   18.58  fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
   18.59      if is_fact fact_names ss then
   18.60 @@ -425,13 +425,13 @@
   18.61  
   18.62  val indent_size = 2
   18.63  
   18.64 -fun string_for_proof ctxt type_enc lam_trans i n proof =
   18.65 +fun string_of_proof ctxt type_enc lam_trans i n proof =
   18.66    let
   18.67      val register_fixes = map Free #> fold Variable.auto_fixes
   18.68      fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
   18.69      fun of_indent ind = replicate_string (ind * indent_size) " "
   18.70      fun of_moreover ind = of_indent ind ^ "moreover\n"
   18.71 -    fun of_label l = if l = no_label then "" else string_for_label l ^ ": "
   18.72 +    fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
   18.73      fun of_obtain qs nr =
   18.74        (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
   18.75           "ultimately "
   18.76 @@ -558,7 +558,7 @@
   18.77            Proof (fix, do_assms assms, map do_step steps)
   18.78    in do_proof proof end
   18.79  
   18.80 -fun prefix_for_depth n = replicate_string (n + 1)
   18.81 +fun prefix_of_depth n = replicate_string (n + 1)
   18.82  
   18.83  val relabel_proof =
   18.84    let
   18.85 @@ -566,7 +566,7 @@
   18.86        if l = no_label then
   18.87          old
   18.88        else
   18.89 -        let val l' = (prefix_for_depth depth prefix, next) in
   18.90 +        let val l' = (prefix_of_depth depth prefix, next) in
   18.91            (l', (l, l') :: subst, next + 1)
   18.92          end
   18.93      fun do_facts subst =
   18.94 @@ -677,7 +677,7 @@
   18.95                  (case resolve_conjecture ss of
   18.96                     [j] =>
   18.97                     if j = length hyp_ts then NONE
   18.98 -                   else SOME (raw_label_for_name name, nth hyp_ts j)
   18.99 +                   else SOME (raw_label_of_name name, nth hyp_ts j)
  18.100                   | _ => NONE)
  18.101                | _ => NONE)
  18.102          val bot = atp_proof |> List.last |> #1
  18.103 @@ -808,8 +808,8 @@
  18.104                    (if isar_proofs = SOME true then isar_compress else 1000.0))
  18.105            |>> clean_up_labels_in_proof
  18.106          val isar_text =
  18.107 -          string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
  18.108 -                           isar_proof
  18.109 +          string_of_proof ctxt type_enc lam_trans subgoal subgoal_count
  18.110 +                          isar_proof
  18.111        in
  18.112          case isar_text of
  18.113            "" =>
    19.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed May 15 17:27:24 2013 +0200
    19.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed May 15 17:43:42 2013 +0200
    19.3 @@ -74,7 +74,7 @@
    19.4      val birth_time = Time.now ()
    19.5      val death_time = Time.+ (birth_time, hard_timeout)
    19.6      val max_facts =
    19.7 -      max_facts |> the_default (default_max_facts_for_prover ctxt slice name)
    19.8 +      max_facts |> the_default (default_max_facts_of_prover ctxt slice name)
    19.9      val num_facts = length facts |> not only ? Integer.min max_facts
   19.10      fun desc () =
   19.11        prover_description ctxt params name num_facts subgoal subgoal_count goal
   19.12 @@ -219,7 +219,7 @@
   19.13              case max_facts of
   19.14                SOME n => n
   19.15              | NONE =>
   19.16 -              0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice)
   19.17 +              0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice)
   19.18                          provers
   19.19                  |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
   19.20          in