1.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:12:21 2009 -0700
     1.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Wed Apr 22 07:20:13 2009 -0700
     1.3 @@ -8,7 +8,14 @@
     1.4  
     1.5  val HOLCF_ss = @{simpset};
     1.6  
     1.7 -structure Domain_Theorems = struct
     1.8 +signature DOMAIN_THEOREMS =
     1.9 +sig
    1.10 +  val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
    1.11 +  val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
    1.12 +end;
    1.13 +
    1.14 +structure Domain_Theorems : DOMAIN_THEOREMS =
    1.15 +struct
    1.16  
    1.17  val quiet_mode = ref false;
    1.18  val trace_domain = ref false;