--- a/src/Pure/codegen.ML Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/codegen.ML Sat Mar 20 17:33:11 2010 +0100
@@ -474,7 +474,7 @@
(**** retrieve definition of constant ****)
fun is_instance T1 T2 =
- Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT T2);
+ Type.raw_instance (T1, if null (OldTerm.typ_tfrees T2) then T2 else Logic.varifyT_global T2);
fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));