# HG changeset patch
# User blanchet
# Date 1280248690 -7200
# Node ID e4a95eb5530e7925af8957af8e2cba7ae6dd4d39
# Parent  962b0a7f544b152c65e7b275f43f987f8c9e6cf2
get rid of "FOLClause" (obsoleted by FOF-enabled "FOLFormula")

diff -r 962b0a7f544b -r e4a95eb5530e src/HOL/Tools/ATP_Manager/atp_problem.ML
--- 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
 
diff -r 962b0a7f544b -r e4a95eb5530e src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- 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 *)
 (*********************************************************************)