src/ZF/ind_syntax.ML
changeset 32952 aeb1e44fbc19
parent 32765 3032c0308019
child 32957 675c0c7e6a37
--- a/src/ZF/ind_syntax.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/ind_syntax.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -89,7 +89,7 @@
 	               $ rec_tm))
   in  map mk_intr constructs  end;
 
-fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
+fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);
 
 fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;