# HG changeset patch
# User immler@in.tum.de
# Date 1246353662 -7200
# Node ID 5e97c4abd18e82aae44f188c73c8b8772fd69d43
# Parent  90ec13cf7ab0a6f858baff71a3985b78e66e1c70
fixed: count constants with supplementary lemmas

diff -r 90ec13cf7ab0 -r 5e97c4abd18e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Jun 30 10:59:02 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Jun 30 11:21:02 2009 +0200
@@ -11,8 +11,9 @@
   val prepare_clauses : bool -> thm list -> thm list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
-    ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
-    ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
+    ResHolClause.axiom_name vector *
+      (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
+      ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
 end;
 
 structure ResAtp: RES_ATP =
@@ -550,13 +551,14 @@
     and tycons = type_consts_of_terms thy (ccltms@axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
     val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+    val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
     val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
     val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in
     (Vector.fromList clnames,
-      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   end
 
 end;
diff -r 90ec13cf7ab0 -r 5e97c4abd18e src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 10:59:02 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 11:21:02 2009 +0200
@@ -36,10 +36,12 @@
        clause list * (thm * (axiom_name * clause_id)) list * string list ->
        clause list
   val tptp_write_file: bool -> Path.T ->
-    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+    clause list * clause list * clause list * clause list *
+    ResClause.classrelClause list * ResClause.arityClause list ->
     int * int
   val dfg_write_file: bool -> Path.T ->
-    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+    clause list * clause list * clause list * clause list *
+    ResClause.classrelClause list * ResClause.arityClause list ->
     int * int
 end
 
@@ -459,11 +461,11 @@
   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
                 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
 
-fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
+fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   if minimize_applies then
      let val (const_min_arity, const_needs_hBOOL) =
           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
-       |> fold count_constants_clause axclauses
+       |> fold count_constants_clause extra_clauses
        |> fold count_constants_clause helper_clauses
      val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
      in (const_min_arity, const_needs_hBOOL) end
@@ -473,7 +475,8 @@
 
 fun tptp_write_file t_full file clauses =
   let
-    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val (conjectures, axclauses, _, helper_clauses,
+      classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
@@ -494,7 +497,8 @@
 
 fun dfg_write_file t_full file clauses =
   let
-    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val (conjectures, axclauses, _, helper_clauses,
+      classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)