src/Tools/code/code_funcgr.ML
changeset 25597 34860182b250
parent 25485 33840a854e63
child 26331 92120667172f
     1.1 --- a/src/Tools/code/code_funcgr.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
     1.5      fun all_classparams tyco class =
     1.6        these (try (#params o AxClass.get_info thy) class)
     1.7 -      |> map (fn (c, _) => Class.param_of_inst thy (c, tyco))
     1.8 +      |> map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
     1.9    in
    1.10      Symtab.empty
    1.11      |> fold (fn (tyco, class) =>
    1.12 @@ -211,7 +211,7 @@
    1.13        |> resort_funcss thy algebra funcgr
    1.14        |> filter_out (can (Graph.get_node funcgr) o fst);
    1.15      fun typ_func c [] = Code.default_typ thy c
    1.16 -      | typ_func c (thms as thm :: _) = case Class.inst_of_param thy c
    1.17 +      | typ_func c (thms as thm :: _) = case AxClass.inst_of_param thy c
    1.18           of SOME (c', tyco) => 
    1.19                let
    1.20                  val (_, ty) = CodeUnit.head_func thm;