equal
deleted
inserted
replaced
117 given by the user |
117 given by the user |
118 *) |
118 *) |
119 fun define_raw_perms (dt_info : Datatype_Aux.info) thy = |
119 fun define_raw_perms (dt_info : Datatype_Aux.info) thy = |
120 let |
120 let |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
121 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
122 val dt_nos = length descr |
122 val dt_nos = length dt_descr |
123 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
123 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
124 val full_tnames = List.take (all_full_tnames, dt_nos); |
124 val full_tnames = List.take (all_full_tnames, dt_nos); |
125 |
125 |
126 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
126 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
127 |
127 |