equal
deleted
inserted
replaced
101 |
101 |
102 |
102 |
103 (* user_dt_nos refers to the number of "un-unfolded" datatypes |
103 (* user_dt_nos refers to the number of "un-unfolded" datatypes |
104 given by the user |
104 given by the user |
105 *) |
105 *) |
106 fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy = |
106 fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = |
107 let |
107 let |
108 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
108 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
109 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
109 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
110 |
110 |
111 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
111 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |