--- a/src/HOLCF/Tools/domain/domain_theorems.ML Wed Apr 22 07:12:21 2009 -0700
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Wed Apr 22 07:20:13 2009 -0700
@@ -8,7 +8,14 @@
val HOLCF_ss = @{simpset};
-structure Domain_Theorems = struct
+signature DOMAIN_THEOREMS =
+sig
+ val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory;
+ val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory;
+end;
+
+structure Domain_Theorems : DOMAIN_THEOREMS =
+struct
val quiet_mode = ref false;
val trace_domain = ref false;