# HG changeset patch
# User blanchet
# Date 1280176525 -7200
# Node ID 43fdc7c259eaf4e283a37803a9b3eaa324b525f0
# Parent  523dc7ad6f9f0d647a212fd98296e7fa4bd6710c
remove obsolete field in record

diff -r 523dc7ad6f9f -r 43fdc7c259ea src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:32:37 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Mon Jul 26 22:35:25 2010 +0200
@@ -218,7 +218,7 @@
   in t |> not (Meson.is_fol_term thy t) ? aux [] end
 
 (* making axiom and conjecture clauses *)
-fun make_clause thy (formula_id, formula_name, kind, t) =
+fun make_clause thy (formula_name, kind, t) =
   let
     (* ### FIXME: perform other transformations previously done by
        "Clausifier.to_nnf", e.g. "HOL.If" *)
@@ -228,15 +228,14 @@
               |> introduce_combinators_in_term thy
     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   in
-    FOLFormula {formula_name = formula_name, formula_id = formula_id,
-                combformula = combformula, kind = kind,
-                ctypes_sorts = ctypes_sorts}
+    FOLFormula {formula_name = formula_name, combformula = combformula,
+                kind = kind, ctypes_sorts = ctypes_sorts}
   end
 
 fun make_axiom_clause thy (name, th) =
-  (name, make_clause thy (0, name, Axiom, prop_of th))
+  (name, make_clause thy (name, Axiom, prop_of th))
 fun make_conjecture_clauses thy ts =
-  map2 (fn j => fn t => make_clause thy (j, "conjecture", Conjecture, t))
+  map2 (fn j => fn t => make_clause thy (Int.toString j, Conjecture, t))
        (0 upto length ts - 1) ts
 
 (** Helper clauses **)
diff -r 523dc7ad6f9f -r 43fdc7c259ea src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:32:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Mon Jul 26 22:35:25 2010 +0200
@@ -23,7 +23,6 @@
 
   datatype fol_formula =
     FOLFormula of {formula_name: string,
-                   formula_id: int,
                    kind: kind,
                    combformula: (name, combterm) formula,
                    ctypes_sorts: typ list}
@@ -162,7 +161,6 @@
 
 datatype fol_formula =
   FOLFormula of {formula_name: string,
-                 formula_id: int,
                  kind: kind,
                  combformula: (name, combterm) formula,
                  ctypes_sorts: typ list}
@@ -246,8 +244,8 @@
        |> mk_adisjunction)
 
 fun problem_line_for_conjecture full_types
-        (FOLFormula {formula_id, kind, combformula, ...}) =
-  Fof (conjecture_prefix ^ Int.toString formula_id, kind,
+        (FOLFormula {formula_name, kind, combformula, ...}) =
+  Fof (conjecture_prefix ^ formula_name, kind,
        formula_for_combformula full_types combformula)
 
 fun atp_free_type_literals_for_conjecture (FOLFormula {ctypes_sorts, ...}) =