equal
deleted
inserted
replaced
647 val _ = Theory.requires thy "Datatype" "datatype definitions"; |
647 val _ = Theory.requires thy "Datatype" "datatype definitions"; |
648 |
648 |
649 (* this theory is used just for parsing *) |
649 (* this theory is used just for parsing *) |
650 val tmp_thy = thy |> |
650 val tmp_thy = thy |> |
651 Theory.copy |> |
651 Theory.copy |> |
652 Sign.add_types (map (fn (tvs, tname, mx, _) => |
652 Sign.add_types_global (map (fn (tvs, tname, mx, _) => |
653 (tname, length tvs, mx)) dts); |
653 (tname, length tvs, mx)) dts); |
654 |
654 |
655 val (tyvars, _, _, _)::_ = dts; |
655 val (tyvars, _, _, _)::_ = dts; |
656 val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => |
656 val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => |
657 let val full_tname = Sign.full_name tmp_thy tname |
657 let val full_tname = Sign.full_name tmp_thy tname |