599 | classrel (Instance ((_, tyco), lss), _) class = |
599 | classrel (Instance ((_, tyco), lss), _) class = |
600 Instance ((class, tyco), lss); |
600 Instance ((class, tyco), lss); |
601 fun constructor tyco lss class = |
601 fun constructor tyco lss class = |
602 Instance ((class, tyco), (map o map) fst lss); |
602 Instance ((class, tyco), (map o map) fst lss); |
603 fun variable (TFree (v, sort)) = |
603 fun variable (TFree (v, sort)) = |
604 map_index (fn (n, class) => (Lookup ([], (v, (n, length sort))), class)) |
604 let val op_sort = operational_sort_of thy sort |
605 (operational_sort_of thy sort); |
605 in map_index (fn (n, class) => (Lookup ([], (v, (n, length op_sort))), class)) op_sort end; |
606 in |
606 in |
607 Sorts.of_sort_derivation pp algebra |
607 Sorts.of_sort_derivation pp algebra |
608 {classrel = classrel, constructor = constructor, variable = variable} |
608 {classrel = classrel, constructor = constructor, variable = variable} |
609 (Type.no_tvars typ_ctxt, operational_sort_of thy sort_decl) |
609 (Type.no_tvars typ_ctxt, operational_sort_of thy sort_decl) |
610 end; |
610 end; |