--- a/src/HOL/Tools/res_clause.ML Mon Aug 28 18:15:32 2006 +0200
+++ b/src/HOL/Tools/res_clause.ML Mon Aug 28 18:16:08 2006 +0200
@@ -6,6 +6,7 @@
Typed equality is treated differently.
*)
+(*FIXME: is this signature necessary? Or maybe define and open a Basic_ResClause?*)
signature RES_CLAUSE =
sig
exception CLAUSE of string * term
@@ -76,7 +77,7 @@
val dfg_arity_clause: arityClause -> string
end;
-structure ResClause : RES_CLAUSE =
+structure ResClause =
struct
(* Added for typed equality *)
@@ -880,8 +881,4 @@
clnames
end;
-
-
-
-
end;