src/Tools/nbe.ML
changeset 41100 6c0940392fb4
parent 41068 7e643e07be7f
child 41118 b290841cd3b0
     1.1 --- a/src/Tools/nbe.ML	Thu Dec 09 09:58:33 2010 +0100
     1.2 +++ b/src/Tools/nbe.ML	Thu Dec 09 17:25:43 2010 +0100
     1.3 @@ -297,10 +297,12 @@
     1.4              then nbe_apps (nbe_fun 0 c) ts'
     1.5              else nbe_apps_constr idx_of c ts'
     1.6        end
     1.7 -    and assemble_idict (DictConst (inst, dss)) =
     1.8 -          assemble_constapp inst dss []
     1.9 -      | assemble_idict (DictVar (supers, (v, (n, _)))) =
    1.10 -          fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
    1.11 +    and assemble_classrels classrels =
    1.12 +      fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
    1.13 +    and assemble_idict (Dict_Const (classrels, (inst, dss))) =
    1.14 +          assemble_classrels classrels (assemble_constapp inst dss [])
    1.15 +      | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
    1.16 +          assemble_classrels classrels (nbe_dict v n);
    1.17  
    1.18      fun assemble_iterm constapp =
    1.19        let