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 63073 413184c7a2a2
parent 62539 00f8bca4aba0
child 63156 3cb84e4469a7 
--- a/src/Tools/Code/code_thingol.ML	Wed May 04 10:19:01 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon May 09 14:37:47 2016 +0200
@@ -574,7 +574,7 @@
       let
         val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
         val dom_length = length (fst (strip_type ty))
-        val thm = Axclass.unoverload_conv thy (Thm.cterm_of ctxt raw_const);
+        val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const);
         val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in
isabelle