diff -r 4c98517601ce -r 33840a854e63 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:40 2007 +0100
+++ b/src/Tools/code/code_thingol.ML	Wed Nov 28 09:01:42 2007 +0100
@@ -461,7 +461,7 @@
     fun exprgen_classparam_inst (c, ty) =
       let
         val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
-        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
+        val thm = Class.unoverload_conv thy (Thm.cterm_of thy c_inst);
         val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in