equal
deleted
inserted
replaced
31 let |
31 let |
32 val defaultS = Sign.defaultS sg; |
32 val defaultS = Sign.defaultS sg; |
33 val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of |
33 val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of |
34 [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
34 [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); |
35 val test_dupl_cons = |
35 val test_dupl_cons = |
36 (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of |
36 (case duplicates (op =) (map (Binding.name_of o first) (flat cons'')) of |
37 [] => false | dups => error ("Duplicate constructors: " |
37 [] => false | dups => error ("Duplicate constructors: " |
38 ^ commas_quote dups)); |
38 ^ commas_quote dups)); |
39 val test_dupl_sels = |
39 val test_dupl_sels = |
40 (case duplicates (op =) (map Binding.name_of (List.mapPartial second |
40 (case duplicates (op =) (map Binding.name_of (map_filter second |
41 (List.concat (map second (List.concat cons''))))) of |
41 (maps second (flat cons'')))) of |
42 [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); |
42 [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); |
43 val test_dupl_tvars = |
43 val test_dupl_tvars = |
44 exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of |
44 exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of |
45 [] => false | dups => error("Duplicate type arguments: " |
45 [] => false | dups => error("Duplicate type arguments: " |
46 ^commas_quote dups)) (map snd dtnvs); |
46 ^commas_quote dups)) (map snd dtnvs); |
140 thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs |
140 thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs |
141 ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); |
141 ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); |
142 in |
142 in |
143 theorems_thy |
143 theorems_thy |
144 |> Sign.add_path (Long_Name.base_name comp_dnam) |
144 |> Sign.add_path (Long_Name.base_name comp_dnam) |
145 |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |
145 |> (snd o (PureThy.add_thmss [((Binding.name "rews", flat rewss @ take_rews), [])])) |
146 |> Sign.parent_path |
146 |> Sign.parent_path |
147 end; |
147 end; |
148 |
148 |
149 val add_domain = gen_add_domain Sign.certify_typ; |
149 val add_domain = gen_add_domain Sign.certify_typ; |
150 val add_domain_cmd = gen_add_domain Syntax.read_typ_global; |
150 val add_domain_cmd = gen_add_domain Syntax.read_typ_global; |