| 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;