equal
deleted
inserted
replaced
411 |
411 |
412 fun mk_constr_consts thy vs dtco cos = |
412 fun mk_constr_consts thy vs dtco cos = |
413 let |
413 let |
414 val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos; |
414 val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos; |
415 val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs; |
415 val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs; |
416 in if is_some (try (Code_Unit.constrset_of_consts thy) cs') |
416 in if is_some (try (Code.constrset_of_consts thy) cs') |
417 then SOME cs |
417 then SOME cs |
418 else NONE |
418 else NONE |
419 end; |
419 end; |
420 |
420 |
421 fun add_all_code dtcos thy = |
421 fun add_all_code dtcos thy = |