diff -r a06a2d930a03 -r 0a43cf458998 indrule.ML
--- a/indrule.ML	Tue Sep 06 10:56:54 1994 +0200
+++ b/indrule.ML	Tue Sep 06 13:24:29 1994 +0200
@@ -90,8 +90,8 @@
 
 (*** Prove the simultaneous induction rule ***)
 
-(*Make distinct predicates for each inductive set;
-  Cartesian products in domT should nest ONLY to the left! *)
+(*Make distinct predicates for each inductive set.
+  Splits cartesian products in domT, IF nested to the right! *)
 
 (*Given a recursive set and its domain, return the "split" predicate
   and a conclusion for the simultaneous induction rule*)