Lines Matching defs:type_names
166 message = "name not in type_names"}
175 (* type_names is the list of names of types being defined *)
176 val type_names = map (#type_name) mut_rec_ty_spec
209 type_names
239 It will return 1 for the first element in type_names, 2 for the
251 fun type_num name = type_num_aux name 1 type_names
666 fun get_sum_type {type_names = [], types_made = [], ...} =
668 | get_sum_type {type_names = [], types_made = inl::rest, type_num} =
674 | get_sum_type {type_names = (type_name::type_names),
685 get_sum_type {type_names = type_names,
690 val sum_type = get_sum_type {type_names = type_names,
717 fun get_ins_outs {type_names = [],...} =
723 | get_ins_outs {type_names = [last], sum_types = [ty]} =
728 | get_ins_outs {type_names = [last], sum_types = tys as ty1 :: _} =
737 | get_ins_outs {type_names = type_name :: type_names,
747 val ins_outs = get_ins_outs {type_names = type_names,
757 val Ins_Outs = get_ins_outs{type_names = type_names,sum_types = [sum_type]}
1142 type_names
1151 type_names
1349 type_names)
1367 | mk_rep_abs_cases_prop (type_name :: type_names) =
1369 conj2 = mk_rep_abs_cases_prop type_names}
1372 Body = mk_rep_abs_cases_prop type_names}
1392 | case_induct_concl num (type_name::type_names) =
1393 CONJ (case_thm type_name num) (case_induct_concl (num + 1) type_names)
1395 val inter_case_induct_thm = (DISCH_ALL (case_induct_concl 1 type_names))
1427 type_names