author blanchet Tue, 27 Jul 2010 18:38:10 +0200 changeset 38024 e4a95eb5530e parent 38023 962b0a7f544b child 38025 b660597a6796
get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")
```--- a/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:33:10 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_problem.ML	Tue Jul 27 18:38:10 2010 +0200
@@ -7,8 +7,6 @@

signature ATP_PROBLEM =
sig
-  type kind = Metis_Clauses.kind
-
datatype 'a fo_term = ATerm of 'a * 'a fo_term list
datatype quantifier = AForall | AExists
datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff
@@ -17,6 +15,7 @@
AConn of connective * ('a, 'b) formula list |
APred of 'b

+  datatype kind = Axiom | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list

@@ -35,8 +34,6 @@

open Sledgehammer_Util

-type kind = Metis_Clauses.kind
-
(** ATP problem **)

datatype 'a fo_term = ATerm of 'a * 'a fo_term list
@@ -47,6 +44,7 @@
AConn of connective * ('a, 'b) formula list |
APred of 'b

+datatype kind = Axiom | Conjecture
datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
type 'a problem = (string * 'a problem_line list) list
```
```--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 18:33:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 18:38:10 2010 +0200
@@ -9,7 +9,6 @@
signature METIS_CLAUSES =
sig
type name = string * string
-  datatype kind = Axiom | Conjecture
datatype type_literal =
TyLitVar of name * name |
TyLitFree of name * name
@@ -29,9 +28,6 @@
CombVar of name * combtyp |
CombApp of combterm * combterm
datatype fol_literal = FOLLiteral of bool * combterm
-  datatype fol_clause =
-    FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                  literals: fol_literal list, ctypes_sorts: typ list}

val type_wrapper_name : string
val bound_var_prefix : string
@@ -228,8 +224,6 @@

type name = string * string

-datatype kind = Axiom | Conjecture
-
(**** Isabelle FOL clauses ****)

(* The first component is the type class; the second is a TVar or TFree. *)
@@ -367,10 +361,6 @@

datatype fol_literal = FOLLiteral of bool * combterm

-datatype fol_clause =
-  FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                literals: fol_literal list, ctypes_sorts: typ list}
-
(*********************************************************************)
(* convert a clause with type Term.term to a clause with type clause *)
(*********************************************************************)```