equal
deleted
inserted
replaced
128 fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background = |
128 fun ml_code_datatype_antiq (raw_tyco, raw_constrs) background = |
129 let |
129 let |
130 val thy = ProofContext.theory_of background; |
130 val thy = ProofContext.theory_of background; |
131 val tyco = Sign.intern_type thy raw_tyco; |
131 val tyco = Sign.intern_type thy raw_tyco; |
132 val constrs = map (Code.check_const thy) raw_constrs; |
132 val constrs = map (Code.check_const thy) raw_constrs; |
133 val constrs' = (map fst o snd o Code.get_datatype thy) tyco; |
133 val constrs' = (map fst o snd o Code.get_type thy) tyco; |
134 val _ = if eq_set (op =) (constrs, constrs') then () |
134 val _ = if eq_set (op =) (constrs, constrs') then () |
135 else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors") |
135 else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors") |
136 val is_first = is_first_occ background; |
136 val is_first = is_first_occ background; |
137 val background' = register_datatype tyco constrs background; |
137 val background' = register_datatype tyco constrs background; |
138 in (print_code is_first (print_datatype tyco constrs), background') end; |
138 in (print_code is_first (print_datatype tyco constrs), background') end; |