src/Tools/nbe.ML
changeset 44788 8b935f1b3cf8
parent 44338 700008399ee5
child 44789 5a062c23c7db
     1.1 --- a/src/Tools/nbe.ML	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Sep 07 13:51:30 2011 +0200
     1.3 @@ -315,7 +315,7 @@
     1.4            let
     1.5              val (t', ts) = Code_Thingol.unfold_app t
     1.6            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
     1.7 -        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
     1.8 +        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
     1.9            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
    1.10            | of_iapp match_cont ((v, _) `|=> t) ts =
    1.11                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
    1.12 @@ -425,7 +425,7 @@
    1.13          val params = Name.invent Name.context "d" (length names);
    1.14          fun mk (k, name) =
    1.15            (name, ([(v, [])],
    1.16 -            [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
    1.17 +            [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params],
    1.18                IVar (SOME (nth params k)))]));
    1.19        in map_index mk names end
    1.20    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
    1.21 @@ -433,8 +433,8 @@
    1.22    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
    1.23        []
    1.24    | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
    1.25 -      [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
    1.26 -        map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
    1.27 +      [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$
    1.28 +        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances
    1.29          @ map (IConst o snd o fst) classparam_instances)]))];
    1.30  
    1.31