src/Tools/nbe.ML
changeset 41118 b290841cd3b0
parent 41100 6c0940392fb4
child 41184 5c6f44d22f51
     1.1 --- a/src/Tools/nbe.ML	Mon Dec 13 10:15:27 2010 +0100
     1.2 +++ b/src/Tools/nbe.ML	Mon Dec 13 22:54:47 2010 +0100
     1.3 @@ -287,7 +287,7 @@
     1.4  
     1.5      fun assemble_constapp c dss ts = 
     1.6        let
     1.7 -        val ts' = (maps o map) assemble_idict dss @ ts;
     1.8 +        val ts' = (maps o map) assemble_dict dss @ ts;
     1.9        in case AList.lookup (op =) eqnss' c
    1.10         of SOME (num_args, _) => if num_args <= length ts'
    1.11              then let val (ts1, ts2) = chop num_args ts'
    1.12 @@ -299,10 +299,12 @@
    1.13        end
    1.14      and assemble_classrels classrels =
    1.15        fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
    1.16 -    and assemble_idict (Dict_Const (classrels, (inst, dss))) =
    1.17 -          assemble_classrels classrels (assemble_constapp inst dss [])
    1.18 -      | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
    1.19 -          assemble_classrels classrels (nbe_dict v n);
    1.20 +    and assemble_dict (Dict (classrels, x)) =
    1.21 +          assemble_classrels classrels (assemble_plain_dict x)
    1.22 +    and assemble_plain_dict (Dict_Const (inst, dss)) =
    1.23 +          assemble_constapp inst dss []
    1.24 +      | assemble_plain_dict (Dict_Var (v, (n, _))) =
    1.25 +          nbe_dict v n
    1.26  
    1.27      fun assemble_iterm constapp =
    1.28        let