ind_syntax.ML
changeset 134 4b7da5a895e7
parent 128 89669c58e506
child 182 d5c6d1fb236b
--- 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*)