src/Tools/code/code_thingol.ML
changeset 25597 34860182b250
parent 25485 33840a854e63
child 25621 97ebdbdb0299
     1.1 --- a/src/Tools/code/code_thingol.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -461,7 +461,7 @@
     1.4      fun exprgen_classparam_inst (c, ty) =
     1.5        let
     1.6          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
     1.7 -        val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
     1.8 +        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
     1.9          val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
    1.10            o Logic.dest_equals o Thm.prop_of) thm;
    1.11        in