src/Tools/Code/code_thingol.ML

 and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
   fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
   let
-    val pp = Syntax.pp_global thy;
     datatype typarg =
         Global of (class * string) * typarg list list
       | Local of (class * class) list * (string * (int * sort));
     fun class_relation (Global ((_, tyco), yss), _) class =
           Global ((class, tyco), yss)

       Global ((class, tyco), (map o map) fst yss);
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val typargs = Sorts.of_sort_derivation pp algebra
+    val typargs = Sorts.of_sort_derivation algebra
       {class_relation = class_relation, type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
     fun mk_dict (Global (inst, yss)) =
           ensure_inst thy algbr funcgr inst