removed the (apparently pointless) signature constraint
authorpaulson
Mon Aug 28 18:16:08 2006 +0200 (2006-08-28)
changeset 2042235a6a4c863f1
parent 20421 d9606c64bc23
child 20423 593053389701
removed the (apparently pointless) signature constraint
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Aug 28 18:15:32 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Aug 28 18:16:08 2006 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  Typed equality is treated differently.
     1.5  *)
     1.6  
     1.7 +(*FIXME: is this signature necessary? Or maybe define and open a Basic_ResClause?*)
     1.8  signature RES_CLAUSE =
     1.9    sig
    1.10    exception CLAUSE of string * term
    1.11 @@ -76,7 +77,7 @@
    1.12    val dfg_arity_clause: arityClause -> string
    1.13  end;
    1.14  
    1.15 -structure ResClause : RES_CLAUSE =
    1.16 +structure ResClause =
    1.17  struct
    1.18  
    1.19  (* Added for typed equality *)
    1.20 @@ -880,8 +881,4 @@
    1.21      clnames
    1.22    end;
    1.23  
    1.24 -
    1.25 -
    1.26 -
    1.27 -
    1.28  end;