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