equal
deleted
inserted
replaced
98 let |
98 let |
99 |
99 |
100 val (_,thy1) = |
100 val (_,thy1) = |
101 fold_map (fn ak => fn thy => |
101 fold_map (fn ak => fn thy => |
102 let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)]) |
102 let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)]) |
103 val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy; |
103 val (dt_names, thy1) = Datatype.add_datatype Datatype_Aux.default_config [dt] thy; |
104 |
104 |
105 val injects = maps (#inject o Datatype.the_info thy1) dt_names; |
105 val injects = maps (#inject o Datatype_Data.the_info thy1) dt_names; |
106 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
106 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
107 val ak_sign = Sign.intern_const thy1 ak |
107 val ak_sign = Sign.intern_const thy1 ak |
108 |
108 |
109 val inj_type = @{typ nat} --> ak_type |
109 val inj_type = @{typ nat} --> ak_type |
110 val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool} |
110 val inj_on_type = inj_type --> @{typ "nat set"} --> @{typ bool} |