--- 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;