diff -r 92d7d8e4f1bf -r 291934bac95e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 06 15:58:56 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.cterm_of thy raw_const);
+        val thm = Axclass.unoverload_conv thy (Thm.global_cterm_of thy raw_const);
         val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in