Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/code/code_thingol.ML
changeset 25485 33840a854e63
parent 25042 a33b78d63114
child 25597 34860182b250 
--- 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
isabelle