1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:58 2011 +0200
     1.3 @@ -61,6 +61,16 @@
     1.4  (* experimental *)
     1.5  val generate_useful_info = false
     1.6  
     1.7 +fun useful_isabelle_info s =
     1.8 +  if generate_useful_info then
     1.9 +    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    1.10 +  else
    1.11 +    NONE
    1.12 +
    1.13 +val intro_info = useful_isabelle_info "intro"
    1.14 +val elim_info = useful_isabelle_info "elim"
    1.15 +val simp_info = useful_isabelle_info "simp"
    1.16 +
    1.17  (* Readable names are often much shorter, especially if types are mangled in
    1.18     names. Also, the logic for generating legal SNARK sort names is only
    1.19     implemented for readable names. Finally, readable names are, well, more
    1.20 @@ -714,7 +724,7 @@
    1.21    in
    1.22      Formula (helper_prefix ^ "ti_ti", Axiom,
    1.23               AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
    1.24 -             |> close_formula_universally, NONE, NONE)
    1.25 +             |> close_formula_universally, simp_info, NONE)
    1.26    end
    1.27  
    1.28  fun helper_facts_for_sym ctxt type_sys (s, {typ, ...} : sym_info) =
    1.29 @@ -874,8 +884,6 @@
    1.30    |> bound_atomic_types type_sys atomic_types
    1.31    |> close_formula_universally
    1.32  
    1.33 -fun useful_isabelle_info s = SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    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 @@ -885,14 +893,11 @@
    1.39                       else string_of_int j ^ "_") ^
    1.40             ascii_of name,
    1.41             kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
    1.42 -           if generate_useful_info then
    1.43 -             case locality of
    1.44 -               Intro => useful_isabelle_info "intro"
    1.45 -             | Elim => useful_isabelle_info "elim"
    1.46 -             | Simp => useful_isabelle_info "simp"
    1.47 -             | _ => NONE
    1.48 -           else
    1.49 -             NONE)
    1.50 +           case locality of
    1.51 +             Intro => intro_info
    1.52 +           | Elim => elim_info
    1.53 +           | Simp => simp_info
    1.54 +           | _ => NONE)
    1.55  
    1.56  fun formula_line_for_class_rel_clause (ClassRelClause {name, subclass,
    1.57                                                         superclass, ...}) =
    1.58 @@ -900,7 +905,7 @@
    1.59      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
    1.60               AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
    1.61                                 AAtom (ATerm (superclass, [ty_arg]))])
    1.62 -             |> close_formula_universally, NONE, NONE)
    1.63 +             |> close_formula_universally, intro_info, NONE)
    1.64    end
    1.65  
    1.66  fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
    1.67 @@ -915,7 +920,7 @@
    1.68                            o fo_literal_from_arity_literal) premLits)
    1.69                      (formula_from_fo_literal
    1.70                           (fo_literal_from_arity_literal conclLit))
    1.71 -           |> close_formula_universally, NONE, NONE)
    1.72 +           |> close_formula_universally, intro_info, NONE)
    1.73  
    1.74  fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
    1.75          ({name, kind, combformula, ...} : translated_formula) =
    1.76 @@ -1050,7 +1055,7 @@
    1.77               |> n > 1 ? bound_atomic_types type_sys (atyps_of T)
    1.78               |> close_formula_universally
    1.79               |> maybe_negate,
    1.80 -             NONE, NONE)
    1.81 +             intro_info, NONE)
    1.82    end
    1.83  
    1.84  fun formula_lines_for_tag_sym_decl ctxt conj_sym_kind nonmono_Ts type_sys n s
    1.85 @@ -1079,7 +1084,7 @@
    1.86        if should_encode res_T then
    1.87          cons (Formula (ident_base ^ "_res", kind,
    1.88                         eq [tag_with res_T (const bounds), const bounds],
    1.89 -                       NONE, NONE))
    1.90 +                       simp_info, NONE))
    1.91        else
    1.92          I
    1.93      fun add_formula_for_arg k =
    1.94 @@ -1091,7 +1096,7 @@
    1.95                             eq [const (bounds1 @ tag_with arg_T bound ::
    1.96                                        bounds2),
    1.97                                 const bounds],
    1.98 -                           NONE, NONE))
    1.99 +                           simp_info, NONE))
   1.100            | _ => raise Fail "expected nonempty tail"
   1.101          else
   1.102            I