src/Tools/nbe.ML
changeset 62539 00f8bca4aba0
parent 61268 abe08fb15a12
child 62958 b41c1cb5e251
--- a/src/Tools/nbe.ML	Tue Mar 08 21:07:47 2016 +0100
+++ b/src/Tools/nbe.ML	Tue Mar 08 21:07:48 2016 +0100
@@ -311,8 +311,8 @@
           assemble_classrels classrels (assemble_plain_dict x)
     and assemble_plain_dict (Dict_Const (inst, dss)) =
           assemble_constapp (Class_Instance inst) dss []
-      | assemble_plain_dict (Dict_Var (v, (n, _))) =
-          nbe_dict v n
+      | assemble_plain_dict (Dict_Var { var, index, ... }) =
+          nbe_dict var index
 
     fun assemble_iterm constapp =
       let