equal
deleted
inserted
replaced
99 let |
99 let |
100 |
100 |
101 val (_,thy1) = |
101 val (_,thy1) = |
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 ({inject,case_thms,...},thy1) = Datatype.add_datatype |
104 val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype |
105 Datatype.default_config [ak] [dt] thy |
105 Datatype.default_config [ak] [dt] thy |
106 val inject_flat = flat inject |
106 val inject_flat = flat inject |
107 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
107 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
108 val ak_sign = Sign.intern_const thy1 ak |
108 val ak_sign = Sign.intern_const thy1 ak |
109 |
109 |