# HG changeset patch
# User wenzelm
# Date 1254346237 -7200
# Node ID a0f38d8d633a8b9e7e1561f10a3aaaa72f684efe
# Parent  7b100d30eb32d6a2f569a6998b837a9e35be4c9a
Sorts.of_sort_derivation: no pp here;

diff -r 7b100d30eb32 -r a0f38d8d633a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Sep 30 23:28:54 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML	Wed Sep 30 23:30:37 2009 +0200
@@ -403,7 +403,7 @@
         @ (maps o maps) fst xs;
     fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
   in
-    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
+    flat (Sorts.of_sort_derivation algebra
       { class_relation = class_relation, type_constructor = type_constructor,
         type_variable = type_variable } (T, proj_sort sort)
        handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
diff -r 7b100d30eb32 -r a0f38d8d633a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 30 23:28:54 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 30 23:30:37 2009 +0200
@@ -750,7 +750,6 @@
   #>> (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));
@@ -764,7 +763,7 @@
       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;