1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 21 17:17:39 2011 +0200
     1.3 @@ -1474,9 +1474,9 @@
     1.4  fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
     1.5    | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
     1.6      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
     1.7 -fun is_var_nonmonotonic_in_formula _ _ (SOME false) _ = false
     1.8 -  | is_var_nonmonotonic_in_formula pos phi _ name =
     1.9 +fun should_predicate_on_var_in_formula pos phi (SOME true) name =
    1.10      formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.11 +  | should_predicate_on_var_in_formula _ _ _ _ = true
    1.12  
    1.13  fun mk_const_aterm format type_sys x T_args args =
    1.14    ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
    1.15 @@ -1548,34 +1548,33 @@
    1.16          end
    1.17        | do_formula pos (AConn conn) = aconn_map pos do_formula conn
    1.18        | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
    1.19 -  in do_formula o SOME end
    1.20 +  in do_formula end
    1.21  
    1.22  fun bound_tvars type_sys Ts =
    1.23    mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
    1.24                  (type_literals_for_types type_sys add_sorts_on_tvar Ts))
    1.25  
    1.26 -fun formula_for_fact ctxt format nonmono_Ts type_sys
    1.27 -                     ({combformula, atomic_types, ...} : translated_formula) =
    1.28 -  combformula
    1.29 -  |> close_combformula_universally
    1.30 -  |> formula_from_combformula ctxt format nonmono_Ts type_sys
    1.31 -                              is_var_nonmonotonic_in_formula true
    1.32 -  |> bound_tvars type_sys atomic_types
    1.33 -  |> close_formula_universally
    1.34 -
    1.35  (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    1.36     of monomorphization). The TPTP explicitly forbids name clashes, and some of
    1.37     the remote provers might care. *)
    1.38 -fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
    1.39 -                          (j, formula as {name, locality, kind, ...}) =
    1.40 -  Formula (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^
    1.41 -           encode name,
    1.42 -           kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
    1.43 -           case locality of
    1.44 -             Intro => intro_info
    1.45 -           | Elim => elim_info
    1.46 -           | Simp => simp_info
    1.47 -           | _ => NONE)
    1.48 +fun formula_line_for_fact ctxt format prefix encode exporter nonmono_Ts type_sys
    1.49 +                          (j, {name, locality, kind, combformula, atomic_types}) =
    1.50 +  (prefix ^ (if exporter then "" else string_of_int j ^ "_") ^ encode name,
    1.51 +   kind,
    1.52 +   combformula
    1.53 +   |> close_combformula_universally
    1.54 +   |> formula_from_combformula ctxt format nonmono_Ts type_sys
    1.55 +                               should_predicate_on_var_in_formula
    1.56 +                               (if exporter then NONE else SOME true)
    1.57 +   |> bound_tvars type_sys atomic_types
    1.58 +   |> close_formula_universally,
    1.59 +   NONE,
    1.60 +   case locality of
    1.61 +     Intro => intro_info
    1.62 +   | Elim => elim_info
    1.63 +   | Simp => simp_info
    1.64 +   | _ => NONE)
    1.65 +  |> Formula
    1.66  
    1.67  fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
    1.68                                         : class_rel_clause) =
    1.69 @@ -1604,7 +1603,7 @@
    1.70          ({name, kind, combformula, atomic_types, ...} : translated_formula) =
    1.71    Formula (conjecture_prefix ^ name, kind,
    1.72             formula_from_combformula ctxt format nonmono_Ts type_sys
    1.73 -               is_var_nonmonotonic_in_formula false
    1.74 +               should_predicate_on_var_in_formula (SOME false)
    1.75                 (close_combformula_universally combformula)
    1.76             |> bound_tvars type_sys atomic_types
    1.77             |> close_formula_universally, NONE, NONE)
    1.78 @@ -1725,7 +1724,7 @@
    1.79               |> type_pred_combterm ctxt format type_sys res_T
    1.80               |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
    1.81               |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
    1.82 -                                         (K (K (K (K true)))) true
    1.83 +                                         (K (K (K (K true)))) (SOME true)
    1.84               |> n > 1 ? bound_tvars type_sys (atyps_of T)
    1.85               |> close_formula_universally
    1.86               |> maybe_negate,
    1.87 @@ -1859,7 +1858,7 @@
    1.88  val explicit_apply = NONE (* for experimental purposes *)
    1.89  
    1.90  fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys
    1.91 -        freshen_facts readable_names preproc hyp_ts concl_t facts =
    1.92 +        exporter readable_names preproc hyp_ts concl_t facts =
    1.93    let
    1.94      val (format, type_sys) = choose_format [format] type_sys
    1.95      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
    1.96 @@ -1887,7 +1886,7 @@
    1.97                                                 poly_nonmono_Ts type_sys
    1.98      val helper_lines =
    1.99        0 upto length helpers - 1 ~~ helpers
   1.100 -      |> map (formula_line_for_fact ctxt format helper_prefix I false
   1.101 +      |> map (formula_line_for_fact ctxt format helper_prefix I exporter
   1.102                                      poly_nonmono_Ts type_sys)
   1.103        |> (if needs_type_tag_idempotence type_sys then
   1.104              cons (type_tag_idempotence_fact ())
   1.105 @@ -1898,8 +1897,8 @@
   1.106      val problem =
   1.107        [(explicit_declsN, sym_decl_lines),
   1.108         (factsN,
   1.109 -        map (formula_line_for_fact ctxt format fact_prefix ascii_of
   1.110 -                                   freshen_facts nonmono_Ts type_sys)
   1.111 +        map (formula_line_for_fact ctxt format fact_prefix ascii_of exporter
   1.112 +                                   nonmono_Ts type_sys)
   1.113              (0 upto length facts - 1 ~~ facts)),
   1.114         (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
   1.115         (aritiesN, map formula_line_for_arity_clause arity_clauses),

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 21 17:17:38 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 21 17:17:39 2011 +0200
     2.3 @@ -646,7 +646,7 @@
     2.4                  val (atp_problem, pool, conjecture_offset, facts_offset,
     2.5                       fact_names, typed_helpers, sym_tab) =
     2.6                    prepare_atp_problem ctxt format conj_sym_kind prem_kind
     2.7 -                      type_sys true (Config.get ctxt atp_readable_names) true
     2.8 +                      type_sys false (Config.get ctxt atp_readable_names) true
     2.9                        hyp_ts concl_t facts
    2.10                  fun weights () = atp_problem_weights atp_problem
    2.11                  val full_proof = debug orelse isar_proof