src/Pure/display.ML

     | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
     | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
 
   fun less_idx ((x, i):indexname, (y, j):indexname) =
     x < y orelse x = y andalso i < j;
-  val sort_idxs = map (apsnd (sort less_idx));
-  val sort_strs = map (apsnd sort_strings);
+  fun sort_idxs l = map (apsnd (sort less_idx)) l;
+  fun sort_strs l = map (apsnd sort_strings) l;
 
 
   (* prepare atoms *)
 
   fun consts_of t = sort_strs (add_consts (t, []));