HOL/ind_syntax/factors: now returns only factors in the product type that
associate to the right. Previously the proof of the induction rule
crashed on types such as (bool*bool)*bool.

--- a/ind_syntax.ML	Wed Aug 31 17:50:59 1994 +0200
+++ b/ind_syntax.ML	Tue Sep 06 10:54:46 1994 +0200
@@ -59,7 +59,8 @@
 
 fun mk_prod (T1,T2) = Type("*", [T1,T2]);
 
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
+(*Maps the type T1*...*Tn to [T1,...,Tn], if nested to the right*)
+fun factors (Type("*", [T1,T2])) = T1 :: factors T2
   | factors T                    = [T];
 
 (*Make a correctly typed ordered pair*)