src/HOL/Tools/Datatype/datatype_case.ML

         val mk_ty = Datatype_Aux.typ_of_dtyp descr sorts;
         val T = Type (tname, map mk_ty dts);
       in
         SOME {case_name = case_name,
           constructors = map (fn (cname, dts') =>
-            Const (cname, Logic.varifyT (map mk_ty dts' ---> T))) constrs}
+            Const (cname, Logic.varifyT_global (map mk_ty dts' ---> T))) constrs}
       end
   | NONE => NONE;
 
 
 (*---------------------------------------------------------------------------

 fun fresh_constr ty_match ty_inst colty used c =
   let
     val (_, Ty) = dest_Const c
     val Ts = binder_types Ty;
     val names = Name.variant_list used
-      (Datatype_Prop.make_tnames (map Logic.unvarifyT Ts));
+      (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
     val ty = body_type Ty;
     val ty_theta = ty_match ty colty handle Type.TYPE_MATCH =>
       raise CASE_ERROR ("type mismatch", ~1)
     val c' = ty_inst ty_theta c
     val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts)