diff -r 6be2f3e03786 -r fcf8024c920d add_ind_def.ML
--- a/add_ind_def.ML	Fri Nov 25 14:39:13 1994 +0100
+++ b/add_ind_def.ML	Fri Nov 25 16:24:18 1994 +0100
@@ -88,9 +88,9 @@
     val z = mk_variant"z" and X = mk_variant"X" and w = mk_variant"w";
 
     (*Probably INCORRECT for mutual recursion!*)
-    val domTs = summands(dest_set (body_type recT));
+    val domTs = summands(dest_setT (body_type recT));
     val dom_sumT = fold_bal mk_sum domTs;
-    val dom_set   = mk_set dom_sumT;
+    val dom_set   = mk_setT dom_sumT;
 
     val freez   = Free(z, dom_sumT)
     and freeX   = Free(X, dom_set);