803 if eq_ityp |
803 if eq_ityp |
804 ((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity, |
804 ((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity, |
805 instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty), |
805 instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty), |
806 (sortctxt', ty')) |
806 (sortctxt', ty')) |
807 then (m, (m', (check_funeqs eqs, (sortctxt', ty')))) |
807 then (m, (m', (check_funeqs eqs, (sortctxt', ty')))) |
808 else error ("inconsistent type for member definition " ^ quote m) |
808 else (m, (m', (check_funeqs eqs, (sortctxt', ty')))) |
|
809 (* error ("inconsistent type for member definition " ^ quote m) *) |
809 in Classinst (d, map mk_memdef membrs) end |
810 in Classinst (d, map mk_memdef membrs) end |
810 | check_prep_def modl Classinstmember = |
811 | check_prep_def modl Classinstmember = |
811 error "attempted to add bare class instance member"; |
812 error "attempted to add bare class instance member"; |
812 |
813 |
813 fun postprocess_def (name, Datatype (_, constrs)) = |
814 fun postprocess_def (name, Datatype (_, constrs)) = |