# HG changeset patch
# User huffman
# Date 1242150009 25200
# Node ID 2823f1b6b8607fb9112e1bb711832b3a245dc7b4
# Parent  fc654c95c29e362b6240af01069a0e46891e76dd
export quiet_mode and trace_domain refs for domain package

diff -r fc654c95c29e -r 2823f1b6b860 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue May 12 17:32:50 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue May 12 10:40:09 2009 -0700
@@ -12,6 +12,8 @@
 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;
+  val quiet_mode: bool ref;
+  val trace_domain: bool ref;
 end;
 
 structure Domain_Theorems :> DOMAIN_THEOREMS =