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 59633 a372513af1e2
parent 59621 291934bac95e
child 59795 d453c69596cc 
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:44:57 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 06 23:52:14 2015 +0100
@@ -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.global_cterm_of thy raw_const);
+        val thm = Axclass.unoverload_conv thy (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