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 |
103 val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy; |
104 Datatype.default_config [ak] [dt] thy; |
|
105 |
104 |
106 val injects = maps (#inject o Datatype.the_info thy1) dt_names; |
105 val injects = maps (#inject o Datatype.the_info thy1) dt_names; |
107 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
106 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
108 val ak_sign = Sign.intern_const thy1 ak |
107 val ak_sign = Sign.intern_const thy1 ak |
109 |
108 |