diff -r 18b1ba7cfcfe -r 8b935f1b3cf8 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Wed Sep 07 11:36:39 2011 +0200
+++ b/src/Tools/nbe.ML	Wed Sep 07 13:51:30 2011 +0200
@@ -315,7 +315,7 @@
           let
             val (t', ts) = Code_Thingol.unfold_app t
           in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
-        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
+        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
           | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
           | of_iapp match_cont ((v, _) `|=> t) ts =
               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -425,7 +425,7 @@
         val params = Name.invent Name.context "d" (length names);
         fun mk (k, name) =
           (name, ([(v, [])],
-            [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+            [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params],
               IVar (SOME (nth params k)))]));
       in map_index mk names end
   | eqns_of_stmt (_, Code_Thingol.Classrel _) =
@@ -433,8 +433,8 @@
   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
       []
   | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
-      [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
-        map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+      [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$
+        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances
         @ map (IConst o snd o fst) classparam_instances)]))];