# HG changeset patch
# User blanchet
# Date 1277741740 -7200
# Node ID 537beae999d738d897218012be84ff19c9c2a27b
# Parent  bcb19259f92a8a07e19138c2659dec0f5a22a2de
remove obsolete component of CNF clause tuple (and reorder it)

diff -r bcb19259f92a -r 537beae999d7 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jun 28 18:08:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Jun 28 18:15:40 2010 +0200
@@ -7,13 +7,12 @@
 
 signature CLAUSIFIER =
 sig
-  type cnf_thm = thm * ((string * int) * thm)
-
   val cnf_axiom: theory -> thm -> thm list
   val multi_base_blacklist: string list
   val is_theorem_bad_for_atps: thm -> bool
   val type_has_topsort: typ -> bool
-  val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
+  val cnf_rules_pairs :
+    theory -> (string * thm) list -> ((string * int) * thm) list
   val neg_clausify: thm -> thm list
   val neg_conjecture_clauses:
     Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -22,8 +21,6 @@
 structure Clausifier : CLAUSIFIER =
 struct
 
-type cnf_thm = thm * ((string * int) * thm)
-
 val type_has_topsort = Term.exists_subtype
   (fn TFree (_, []) => true
     | TVar (_, []) => true
@@ -324,7 +321,7 @@
   let
     fun do_one _ [] = []
       | do_one ((name, k), th) (cls :: clss) =
-        (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+        ((name, k), cls) :: do_one ((name, k + 1), th) clss
     fun do_all pairs [] = pairs
       | do_all pairs ((name, th) :: ths) =
         let
diff -r bcb19259f92a -r 537beae999d7 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jun 28 18:08:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Jun 28 18:15:40 2010 +0200
@@ -8,7 +8,6 @@
 
 signature METIS_CLAUSES =
 sig
-  type cnf_thm = Clausifier.cnf_thm
   type name = string * string
   type name_pool = string Symtab.table * string Symtab.table
   datatype kind = Axiom | Conjecture
@@ -78,7 +77,8 @@
   val tvar_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
   val prepare_clauses :
-    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
+    bool -> thm list -> ((string * int) * thm) list
+    -> ((string * int) * thm) list -> theory
     -> string vector
        * (hol_clause list * hol_clause list * hol_clause list * hol_clause list
           * classrel_clause list * arity_clause list)
@@ -583,9 +583,9 @@
                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   end
 
-fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
+fun add_axiom_clause thy ((name, k), th) (skolem_somes, clss) =
   let
-    val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
+    val (skolem_somes, cls) = make_clause thy (k, name, Axiom, th) skolem_somes
   in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
 
 fun make_axiom_clauses thy clauses =
@@ -610,10 +610,9 @@
 fun count_literal (Literal (_, t)) = count_combterm t
 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
 
-fun raw_cnf_rules_pairs ps = map (fn (name, thm) => (thm, ((name, 0), thm))) ps
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
-  #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)
+  #> (if raw then  map (apfst (rpair 0)) else cnf_rules_pairs thy)
 
 val optional_helpers =
   [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
@@ -642,9 +641,6 @@
       @ (if is_FO then [] else cnf_helper_thms thy false mandatory_helpers)
   in map snd (make_axiom_clauses thy cnfs) end
 
-fun make_clause_table xs =
-  fold (Termtab.update o `(prop_of o fst)) xs Termtab.empty
-
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
@@ -683,6 +679,9 @@
 fun type_consts_of_terms thy ts =
   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
 
+fun make_clause_table xs =
+  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
+
 (* Remove existing axiom clauses from the conjecture clauses, as this can
    dramatically boost an ATP's performance (for some reason). *)
 fun subtract_cls ax_clauses =
@@ -696,7 +695,7 @@
     val ccls = subtract_cls extra_cls goal_cls
     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
     val ccltms = map prop_of ccls
-    and axtms = map (prop_of o #1) extra_cls
+    and axtms = map (prop_of o snd) extra_cls
     val subs = tfree_classes_of_terms ccltms
     and supers = tvar_classes_of_terms axtms
     and tycons = type_consts_of_terms thy (ccltms @ axtms)