equal
deleted
inserted
replaced
50 NONE => NONE |
50 NONE => NONE |
51 | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => |
51 | SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => |
52 if is_some (Codegen.get_assoc_type thy tname) then NONE else |
52 if is_some (Codegen.get_assoc_type thy tname) then NONE else |
53 let |
53 let |
54 val module' = Codegen.if_library |
54 val module' = Codegen.if_library |
55 (Codegen.thyname_of_type tname thy) module; |
55 (Codegen.thyname_of_type thy tname) module; |
56 val node_id = tname ^ " (type)"; |
56 val node_id = tname ^ " (type)"; |
57 val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map |
57 val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map |
58 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) |
58 (Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) |
59 (gr, Ts) |>>> |
59 (gr, Ts) |>>> |
60 Codegen.mk_const_id module' Abs_name |>>> |
60 Codegen.mk_const_id module' Abs_name |>>> |