equal
deleted
inserted
replaced
998 |
998 |
999 val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; |
999 val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0; |
1000 |
1000 |
1001 val qsoty = quote o Syntax.string_of_typ fake_lthy; |
1001 val qsoty = quote o Syntax.string_of_typ fake_lthy; |
1002 |
1002 |
1003 val _ = (case duplicates (op =) unsorted_As of [] => () |
1003 val _ = (case Library.duplicates (op =) unsorted_As of [] => () |
1004 | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^ |
1004 | A :: _ => error ("Duplicate type parameter " ^ qsoty A ^ " in " ^ co_prefix fp ^ |
1005 "datatype specification")); |
1005 "datatype specification")); |
1006 |
1006 |
1007 val bad_args = |
1007 val bad_args = |
1008 map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As |
1008 map (Logic.type_map (singleton (Variable.polymorphic no_defs_lthy0))) unsorted_As |
1011 error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^ |
1011 error ("Locally fixed type argument " ^ qsoty (hd bad_args) ^ " in " ^ co_prefix fp ^ |
1012 "datatype specification"); |
1012 "datatype specification"); |
1013 |
1013 |
1014 val mixfixes = map mixfix_of specs; |
1014 val mixfixes = map mixfix_of specs; |
1015 |
1015 |
1016 val _ = (case duplicates Binding.eq_name fp_bs of [] => () |
1016 val _ = (case Library.duplicates Binding.eq_name fp_bs of [] => () |
1017 | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); |
1017 | b :: _ => error ("Duplicate type name declaration " ^ quote (Binding.name_of b))); |
1018 |
1018 |
1019 val ctr_specss = map ctr_specs_of specs; |
1019 val ctr_specss = map ctr_specs_of specs; |
1020 |
1020 |
1021 val disc_bindingss = map (map disc_of) ctr_specss; |
1021 val disc_bindingss = map (map disc_of) ctr_specss; |