equal
deleted
inserted
replaced
63 let |
63 let |
64 |
64 |
65 val (_,thy1) = |
65 val (_,thy1) = |
66 fold_map (fn ak => fn thy => |
66 fold_map (fn ak => fn thy => |
67 let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) |
67 let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) |
68 val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype_i true false [ak] [dt] thy |
68 val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy |
69 val inject_flat = Library.flat inject |
69 val inject_flat = Library.flat inject |
70 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
70 val ak_type = Type (Sign.intern_type thy1 ak,[]) |
71 val ak_sign = Sign.intern_const thy1 ak |
71 val ak_sign = Sign.intern_const thy1 ak |
72 |
72 |
73 val inj_type = @{typ nat}-->ak_type |
73 val inj_type = @{typ nat}-->ak_type |