1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 06 17:19:34 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 06 17:19:34 2011 +0100
     1.3 @@ -105,17 +105,15 @@
     1.4  type name = string * string
     1.5  
     1.6  (* experimental *)
     1.7 -val generate_useful_info = false
     1.8 +val generate_info = false
     1.9  
    1.10 -fun useful_isabelle_info s =
    1.11 -  if generate_useful_info then
    1.12 -    SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    1.13 -  else
    1.14 -    NONE
    1.15 +fun isabelle_info s =
    1.16 +  if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
    1.17 +  else NONE
    1.18  
    1.19 -val intro_info = useful_isabelle_info "intro"
    1.20 -val elim_info = useful_isabelle_info "elim"
    1.21 -val simp_info = useful_isabelle_info "simp"
    1.22 +val introN = "intro"
    1.23 +val elimN = "elim"
    1.24 +val simpN = "simp"
    1.25  
    1.26  val bound_var_prefix = "B_"
    1.27  val schematic_var_prefix = "V_"
    1.28 @@ -1343,7 +1341,7 @@
    1.29    in
    1.30      Formula (type_tag_idempotence_helper_name, Axiom,
    1.31               AAtom (ATerm (`I tptp_equal, [tag tagged_a, tagged_a]))
    1.32 -             |> close_formula_universally, simp_info, NONE)
    1.33 +             |> close_formula_universally, isabelle_info simpN, NONE)
    1.34    end
    1.35  
    1.36  fun should_specialize_helper type_enc t =
    1.37 @@ -1579,9 +1577,9 @@
    1.38     |> close_formula_universally,
    1.39     NONE,
    1.40     case locality of
    1.41 -     Intro => intro_info
    1.42 -   | Elim => elim_info
    1.43 -   | Simp => simp_info
    1.44 +     Intro => isabelle_info introN
    1.45 +   | Elim => isabelle_info elimN
    1.46 +   | Simp => isabelle_info simpN
    1.47     | _ => NONE)
    1.48    |> Formula
    1.49  
    1.50 @@ -1591,7 +1589,7 @@
    1.51      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
    1.52               AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
    1.53                                 AAtom (ATerm (superclass, [ty_arg]))])
    1.54 -             |> close_formula_universally, intro_info, NONE)
    1.55 +             |> close_formula_universally, isabelle_info introN, NONE)
    1.56    end
    1.57  
    1.58  fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
    1.59 @@ -1606,7 +1604,7 @@
    1.60                            o fo_literal_from_arity_literal) prem_lits)
    1.61                      (formula_from_fo_literal
    1.62                           (fo_literal_from_arity_literal concl_lits))
    1.63 -           |> close_formula_universally, intro_info, NONE)
    1.64 +           |> close_formula_universally, isabelle_info introN, NONE)
    1.65  
    1.66  fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
    1.67          ({name, kind, combformula, atomic_types, ...} : translated_formula) =
    1.68 @@ -1739,7 +1737,7 @@
    1.69               |> n > 1 ? bound_tvars type_enc (atyps_of T)
    1.70               |> close_formula_universally
    1.71               |> maybe_negate,
    1.72 -             intro_info, NONE)
    1.73 +             isabelle_info introN, NONE)
    1.74    end
    1.75  
    1.76  fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
    1.77 @@ -1776,7 +1774,7 @@
    1.78        if should_encode res_T then
    1.79          cons (Formula (ident_base ^ "_res", kind,
    1.80                         eq [tag_with res_T (cst bounds), cst bounds],
    1.81 -                       simp_info, NONE))
    1.82 +                       isabelle_info simpN, NONE))
    1.83        else
    1.84          I
    1.85      fun add_formula_for_arg k =
    1.86 @@ -1787,7 +1785,7 @@
    1.87              cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
    1.88                             eq [cst (bounds1 @ tag_with arg_T bound :: bounds2),
    1.89                                 cst bounds],
    1.90 -                           simp_info, NONE))
    1.91 +                           isabelle_info simpN, NONE))
    1.92            | _ => raise Fail "expected nonempty tail"
    1.93          else
    1.94            I