1.1 --- a/src/Tools/Code/code_preproc.ML	Wed Sep 30 23:28:54 2009 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Sep 30 23:30:37 2009 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4          @ (maps o maps) fst xs;
     1.5      fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
     1.6    in
     1.7 -    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
     1.8 +    flat (Sorts.of_sort_derivation algebra
     1.9        { class_relation = class_relation, type_constructor = type_constructor,
    1.10          type_variable = type_variable } (T, proj_sort sort)
    1.11         handle Sorts.CLASS_ERROR _ => [] (*permissive!*))

     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 30 23:28:54 2009 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 30 23:30:37 2009 +0200
     2.3 @@ -750,7 +750,6 @@
     2.4    #>> (fn sort => (unprefix "'" v, sort))
     2.5  and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) =
     2.6    let
     2.7 -    val pp = Syntax.pp_global thy;
     2.8      datatype typarg =
     2.9          Global of (class * string) * typarg list list
    2.10        | Local of (class * class) list * (string * (int * sort));
    2.11 @@ -764,7 +763,7 @@
    2.12        let
    2.13          val sort' = proj_sort sort;
    2.14        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
    2.15 -    val typargs = Sorts.of_sort_derivation pp algebra
    2.16 +    val typargs = Sorts.of_sort_derivation algebra
    2.17        {class_relation = class_relation, type_constructor = type_constructor,
    2.18         type_variable = type_variable} (ty, proj_sort sort)
    2.19        handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;