--- 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 *)
(*********************************************************************)