1.1 --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:32:37 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:35:25 2010 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4    in t |> not (Meson.is_fol_term thy t) ? aux [] end
     1.5  
     1.6  (* making axiom and conjecture clauses *)
     1.7 -fun make_clause thy (formula_id, formula_name, kind, t) =
     1.8 +fun make_clause thy (formula_name, kind, t) =
     1.9    let
    1.10      (* ### FIXME: perform other transformations previously done by
    1.11         "Clausifier.to_nnf", e.g. "HOL.If" *)
    1.12 @@ -228,15 +228,14 @@
    1.13                |> introduce_combinators_in_term thy
    1.14      val (combformula, ctypes_sorts) = combformula_for_prop thy t []
    1.15    in
    1.16 -    FOLFormula {formula_name = formula_name, formula_id = formula_id,
    1.17 -                combformula = combformula, kind = kind,
    1.18 -                ctypes_sorts = ctypes_sorts}
    1.19 +    FOLFormula {formula_name = formula_name, combformula = combformula,
    1.20 +                kind = kind, ctypes_sorts = ctypes_sorts}
    1.21    end
    1.22  
    1.23  fun make_axiom_clause thy (name, th) =
    1.24 -  (name, make_clause thy (0, name, Axiom, prop_of th))
    1.25 +  (name, make_clause thy (name, Axiom, prop_of th))
    1.26  fun make_conjecture_clauses thy ts =
    1.27 -  map2 (fn j => fn t => make_clause thy (j, "conjecture", Conjecture, t))
    1.28 +  map2 (fn j => fn t => make_clause thy (Int.toString j, Conjecture, t))
    1.29         (0 upto length ts - 1) ts
    1.30  
    1.31  (** Helper clauses **)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:32:37 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:35:25 2010 +0200
     2.3 @@ -23,7 +23,6 @@
     2.4  
     2.5    datatype fol_formula =
     2.6      FOLFormula of {formula_name: string,
     2.7 -                   formula_id: int,
     2.8                     kind: kind,
     2.9                     combformula: (name, combterm) formula,
    2.10                     ctypes_sorts: typ list}
    2.11 @@ -162,7 +161,6 @@
    2.12  
    2.13  datatype fol_formula =
    2.14    FOLFormula of {formula_name: string,
    2.15 -                 formula_id: int,
    2.16                   kind: kind,
    2.17                   combformula: (name, combterm) formula,
    2.18                   ctypes_sorts: typ list}
    2.19 @@ -246,8 +244,8 @@
    2.20         |> mk_adisjunction)
    2.21  
    2.22  fun problem_line_for_conjecture full_types
    2.23 -        (FOLFormula {formula_id, kind, combformula, ...}) =
    2.24 -  Fof (conjecture_prefix ^ Int.toString formula_id, kind,
    2.25 +        (FOLFormula {formula_name, kind, combformula, ...}) =
    2.26 +  Fof (conjecture_prefix ^ formula_name, kind,
    2.27         formula_for_combformula full_types combformula)
    2.28  
    2.29  fun atp_free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =