# HG changeset patch
# User huffman
# Date 1267833588 28800
# Node ID 50ba5010b876aafcf0b1b6ac78654cee3782fc87
# Parent  94bd5188074690709b5b4f4f67ac45af18144a5a
print message when finiteness of domain definition is detected

diff -r 94bd51880746 -r 50ba5010b876 src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:27:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:59:48 2010 -0800
@@ -278,6 +278,9 @@
     val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
     val is_emptys = map warn n__eqs;
     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+    val _ = if is_finite
+            then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+            else ();
   end;
   val _ = trace " Proving finite_ind...";
   val finite_ind =