--- a/src/Tools/Code/code_thingol.ML Wed Jul 08 06:43:30 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Jul 08 08:18:07 2009 +0200
@@ -722,15 +722,15 @@
ensure_inst thy algbr funcgr inst
##>> (fold_map o fold_map) mk_dict yss
#>> (fn (inst, dss) => DictConst (inst, dss))
- | mk_dict (Local (classrels, (v, (k, sort)))) =
+ | mk_dict (Local (classrels, (v, (n, sort)))) =
fold_map (ensure_classrel thy algbr funcgr) classrels
- #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
+ #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
in fold_map mk_dict typargs end;
(* store *)
-structure Program = CodeDataFun
+structure Program = Code_Data_Fun
(
type T = naming * program;
val empty = (empty_naming, Graph.empty);