get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
authorblanchet
Tue Jul 27 18:38:10 2010 +0200 (2010-07-27)
changeset 38024e4a95eb5530e
parent 38023 962b0a7f544b
child 38025 b660597a6796
get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
src/HOL/Tools/ATP_Manager/atp_problem.ML
src/HOL/Tools/Sledgehammer/metis_clauses.ML
     1.1 --- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:33:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:38:10 2010 +0200
     1.3 @@ -7,8 +7,6 @@
     1.4  
     1.5  signature ATP_PROBLEM =
     1.6  sig
     1.7 -  type kind = Metis_Clauses.kind
     1.8 -
     1.9    datatype 'a fo_term = ATerm of 'a * 'a fo_term list
    1.10    datatype quantifier = AForall | AExists
    1.11    datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
    1.12 @@ -17,6 +15,7 @@
    1.13      AConn of connective * ('a, 'b) formula list |
    1.14      APred of 'b
    1.15  
    1.16 +  datatype kind = Axiom | Conjecture
    1.17    datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
    1.18    type 'a problem = (string * 'a problem_line list) list
    1.19  
    1.20 @@ -35,8 +34,6 @@
    1.21  
    1.22  open Sledgehammer_Util
    1.23  
    1.24 -type kind = Metis_Clauses.kind
    1.25 -
    1.26  (** ATP problem **)
    1.27  
    1.28  datatype 'a fo_term = ATerm of 'a * 'a fo_term list
    1.29 @@ -47,6 +44,7 @@
    1.30    AConn of connective * ('a, 'b) formula list |
    1.31    APred of 'b
    1.32  
    1.33 +datatype kind = Axiom | Conjecture
    1.34  datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
    1.35  type 'a problem = (string * 'a problem_line list) list
    1.36  
     2.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 18:33:10 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 18:38:10 2010 +0200
     2.3 @@ -9,7 +9,6 @@
     2.4  signature METIS_CLAUSES =
     2.5  sig
     2.6    type name = string * string
     2.7 -  datatype kind = Axiom | Conjecture
     2.8    datatype type_literal =
     2.9      TyLitVar of name * name |
    2.10      TyLitFree of name * name
    2.11 @@ -29,9 +28,6 @@
    2.12      CombVar of name * combtyp |
    2.13      CombApp of combterm * combterm
    2.14    datatype fol_literal = FOLLiteral of bool * combterm
    2.15 -  datatype fol_clause =
    2.16 -    FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    2.17 -                  literals: fol_literal list, ctypes_sorts: typ list}
    2.18  
    2.19    val type_wrapper_name : string
    2.20    val bound_var_prefix : string
    2.21 @@ -228,8 +224,6 @@
    2.22  
    2.23  type name = string * string
    2.24  
    2.25 -datatype kind = Axiom | Conjecture
    2.26 -
    2.27  (**** Isabelle FOL clauses ****)
    2.28  
    2.29  (* The first component is the type class; the second is a TVar or TFree. *)
    2.30 @@ -367,10 +361,6 @@
    2.31  
    2.32  datatype fol_literal = FOLLiteral of bool * combterm
    2.33  
    2.34 -datatype fol_clause =
    2.35 -  FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
    2.36 -                literals: fol_literal list, ctypes_sorts: typ list}
    2.37 -
    2.38  (*********************************************************************)
    2.39  (* convert a clause with type Term.term to a clause with type clause *)
    2.40  (*********************************************************************)