src/HOL/Tools/res_hol_clause.ML
changeset 31865 5e97c4abd18e
parent 31839 26f18ec0e293
child 31910 a8e9ccfc427a
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 10:59:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 11:21:02 2009 +0200
     1.3 @@ -36,10 +36,12 @@
     1.4         clause list * (thm * (axiom_name * clause_id)) list * string list ->
     1.5         clause list
     1.6    val tptp_write_file: bool -> Path.T ->
     1.7 -    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
     1.8 +    clause list * clause list * clause list * clause list *
     1.9 +    ResClause.classrelClause list * ResClause.arityClause list ->
    1.10      int * int
    1.11    val dfg_write_file: bool -> Path.T ->
    1.12 -    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
    1.13 +    clause list * clause list * clause list * clause list *
    1.14 +    ResClause.classrelClause list * ResClause.arityClause list ->
    1.15      int * int
    1.16  end
    1.17  
    1.18 @@ -459,11 +461,11 @@
    1.19    Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
    1.20                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    1.21  
    1.22 -fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
    1.23 +fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
    1.24    if minimize_applies then
    1.25       let val (const_min_arity, const_needs_hBOOL) =
    1.26            fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
    1.27 -       |> fold count_constants_clause axclauses
    1.28 +       |> fold count_constants_clause extra_clauses
    1.29         |> fold count_constants_clause helper_clauses
    1.30       val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
    1.31       in (const_min_arity, const_needs_hBOOL) end
    1.32 @@ -473,7 +475,8 @@
    1.33  
    1.34  fun tptp_write_file t_full file clauses =
    1.35    let
    1.36 -    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    1.37 +    val (conjectures, axclauses, _, helper_clauses,
    1.38 +      classrel_clauses, arity_clauses) = clauses
    1.39      val (cma, cnh) = count_constants clauses
    1.40      val params = (t_full, cma, cnh)
    1.41      val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
    1.42 @@ -494,7 +497,8 @@
    1.43  
    1.44  fun dfg_write_file t_full file clauses =
    1.45    let
    1.46 -    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
    1.47 +    val (conjectures, axclauses, _, helper_clauses,
    1.48 +      classrel_clauses, arity_clauses) = clauses
    1.49      val (cma, cnh) = count_constants clauses
    1.50      val params = (t_full, cma, cnh)
    1.51      val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)