1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 09:10:13 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     1.3 @@ -63,10 +63,18 @@
     1.4    val skolem_const_prefix : string
     1.5    val old_skolem_const_prefix : string
     1.6    val new_skolem_const_prefix : string
     1.7 +  val type_decl_prefix : string
     1.8 +  val sym_decl_prefix : string
     1.9 +  val preds_sym_formula_prefix : string
    1.10 +  val tags_sym_formula_prefix : string
    1.11    val fact_prefix : string
    1.12    val conjecture_prefix : string
    1.13    val helper_prefix : string
    1.14 +  val class_rel_clause_prefix : string
    1.15 +  val arity_clause_prefix : string
    1.16 +  val tfree_clause_prefix : string
    1.17    val typed_helper_suffix : string
    1.18 +  val untyped_helper_suffix : string
    1.19    val predicator_name : string
    1.20    val app_op_name : string
    1.21    val type_tag_name : string
    1.22 @@ -163,7 +171,8 @@
    1.23  
    1.24  val type_decl_prefix = "ty_"
    1.25  val sym_decl_prefix = "sy_"
    1.26 -val sym_formula_prefix = "sym_"
    1.27 +val preds_sym_formula_prefix = "psy_"
    1.28 +val tags_sym_formula_prefix = "tsy_"
    1.29  val fact_prefix = "fact_"
    1.30  val conjecture_prefix = "conj_"
    1.31  val helper_prefix = "help_"
    1.32 @@ -1627,8 +1636,8 @@
    1.33  
    1.34  fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
    1.35  
    1.36 -fun formula_line_for_pred_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
    1.37 -                                   n s j (s', T_args, T, _, ary, in_conj) =
    1.38 +fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
    1.39 +        type_sys n s j (s', T_args, T, _, ary, in_conj) =
    1.40    let
    1.41      val (kind, maybe_negate) =
    1.42        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
    1.43 @@ -1642,7 +1651,7 @@
    1.44        arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
    1.45                               else NONE)
    1.46    in
    1.47 -    Formula (sym_formula_prefix ^ s ^
    1.48 +    Formula (preds_sym_formula_prefix ^ s ^
    1.49               (if n > 1 then "_" ^ string_of_int j else ""), kind,
    1.50               CombConst ((s, s'), T, T_args)
    1.51               |> fold (curry (CombApp o swap)) bounds
    1.52 @@ -1656,11 +1665,12 @@
    1.53               intro_info, NONE)
    1.54    end
    1.55  
    1.56 -fun formula_lines_for_tag_sym_decl ctxt format conj_sym_kind nonmono_Ts type_sys
    1.57 -        n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
    1.58 +fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind nonmono_Ts
    1.59 +        type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
    1.60    let
    1.61      val ident_base =
    1.62 -      sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "")
    1.63 +      tags_sym_formula_prefix ^ s ^
    1.64 +      (if n > 1 then "_" ^ string_of_int j else "")
    1.65      val (kind, maybe_negate) =
    1.66        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
    1.67        else (Axiom, I)
    1.68 @@ -1730,8 +1740,8 @@
    1.69                     o result_type_of_decl)
    1.70      in
    1.71        (0 upto length decls - 1, decls)
    1.72 -      |-> map2 (formula_line_for_pred_sym_decl ctxt format conj_sym_kind
    1.73 -                                               nonmono_Ts type_sys n s)
    1.74 +      |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
    1.75 +                                                nonmono_Ts type_sys n s)
    1.76      end
    1.77    | Tags (_, _, heaviness) =>
    1.78      (case heaviness of
    1.79 @@ -1739,8 +1749,8 @@
    1.80       | Light =>
    1.81         let val n = length decls in
    1.82           (0 upto n - 1 ~~ decls)
    1.83 -         |> maps (formula_lines_for_tag_sym_decl ctxt format conj_sym_kind
    1.84 -                                                 nonmono_Ts type_sys n s)
    1.85 +         |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind
    1.86 +                                                  nonmono_Ts type_sys n s)
    1.87         end)
    1.88  
    1.89  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts

     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 09:10:13 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     2.3 @@ -262,7 +262,7 @@
     2.4      metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
     2.5    | m_arity_cls (TVarLit ((c, _), (s, _))) =
     2.6      metis_lit false c [Metis_Term.Var s]
     2.7 -(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
     2.8 +(* TrueI is returned as the Isabelle counterpart because there isn't any. *)
     2.9  fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) =
    2.10    (TrueI,
    2.11     Metis_Thm.axiom (Metis_LiteralSet.fromList