52 FIXME: could insert all constant set expressions, e.g. nat->nat.*) |
52 FIXME: could insert all constant set expressions, e.g. nat->nat.*) |
53 fun data_domain co (rec_tms, con_ty_lists) = |
53 fun data_domain co (rec_tms, con_ty_lists) = |
54 let val rec_hds = map head_of rec_tms |
54 let val rec_hds = map head_of rec_tms |
55 val dummy = assert_all is_Const rec_hds |
55 val dummy = assert_all is_Const rec_hds |
56 (fn t => "Datatype set not previously declared as constant: " ^ |
56 (fn t => "Datatype set not previously declared as constant: " ^ |
57 Sign.string_of_term @{theory IFOL} t); |
57 Syntax.string_of_term_global @{theory IFOL} t); |
58 val rec_names = (*nat doesn't have to be added*) |
58 val rec_names = (*nat doesn't have to be added*) |
59 @{const_name nat} :: map (#1 o dest_Const) rec_hds |
59 @{const_name nat} :: map (#1 o dest_Const) rec_hds |
60 val u = if co then @{const QUniv.quniv} else @{const Univ.univ} |
60 val u = if co then @{const QUniv.quniv} else @{const Univ.univ} |
61 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
61 val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms) |
62 (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t |
62 (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t |
70 |
70 |
71 val rec_hds = map head_of rec_tms; |
71 val rec_hds = map head_of rec_tms; |
72 |
72 |
73 val dummy = assert_all is_Const rec_hds |
73 val dummy = assert_all is_Const rec_hds |
74 (fn t => "Datatype set not previously declared as constant: " ^ |
74 (fn t => "Datatype set not previously declared as constant: " ^ |
75 Sign.string_of_term thy t); |
75 Syntax.string_of_term_global thy t); |
76 |
76 |
77 val rec_names = map (#1 o dest_Const) rec_hds |
77 val rec_names = map (#1 o dest_Const) rec_hds |
78 val rec_base_names = map Sign.base_name rec_names |
78 val rec_base_names = map Sign.base_name rec_names |
79 val big_rec_base_name = space_implode "_" rec_base_names |
79 val big_rec_base_name = space_implode "_" rec_base_names |
80 |
80 |