diff -r 85ebb645b1a3 -r 00f8bca4aba0 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Mar 08 21:07:47 2016 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Mar 08 21:07:48 2016 +0100
@@ -87,12 +87,13 @@
           ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          [str (if k = 1 then Name.enforce_case true v ^ "_"
-            else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
+      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
+          [str (if length = 1 then Name.enforce_case true var ^ "_"
+            else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
-      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -398,12 +399,13 @@
           brackify BR ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          str (if k = 1 then "_" ^ Name.enforce_case true v
-            else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
+      | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length }) =
+          str (if length = 1 then "_" ^ Name.enforce_case true var
+            else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
-      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =