# HG changeset patch
# User paulson
# Date 1156781768 -7200
# Node ID 35a6a4c863f1067510d66c06590bc77431516eb1
# Parent  d9606c64bc23b35223b775b541525b5b5762e3ad
removed the (apparently pointless) signature constraint

diff -r d9606c64bc23 -r 35a6a4c863f1 src/HOL/Tools/res_clause.ML
--- 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;