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