src/Tools/Code/code_thingol.ML
changeset 31962 baa8dce5bc45
parent 31957 a9742afd403e
child 32091 30e2ffbba718
child 32123 8bac9ee4b28d
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 08 06:43:30 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Jul 08 08:18:07 2009 +0200
     1.3 @@ -722,15 +722,15 @@
     1.4            ensure_inst thy algbr funcgr inst
     1.5            ##>> (fold_map o fold_map) mk_dict yss
     1.6            #>> (fn (inst, dss) => DictConst (inst, dss))
     1.7 -      | mk_dict (Local (classrels, (v, (k, sort)))) =
     1.8 +      | mk_dict (Local (classrels, (v, (n, sort)))) =
     1.9            fold_map (ensure_classrel thy algbr funcgr) classrels
    1.10 -          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
    1.11 +          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
    1.12    in fold_map mk_dict typargs end;
    1.13  
    1.14  
    1.15  (* store *)
    1.16  
    1.17 -structure Program = CodeDataFun
    1.18 +structure Program = Code_Data_Fun
    1.19  (
    1.20    type T = naming * program;
    1.21    val empty = (empty_naming, Graph.empty);