equal
deleted
inserted
replaced
336 |
336 |
337 fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T) |
337 fun mkName (Type (T,args)) = implode (map mkName args) ^ mkUpper (Long_Name.base_name T) |
338 | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x) |
338 | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x) |
339 | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x); |
339 | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x); |
340 |
340 |
341 fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting; |
341 fun is_datatype thy = is_some o BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting]; |
342 |
342 |
343 fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map} |
343 fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map} |
344 | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n); |
344 | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n); |
345 |
345 |
346 fun gen_constr_destr comp prfx thy (Type (T, [])) = |
346 fun gen_constr_destr comp prfx thy (Type (T, [])) = |