src/Pure/Tools/find_consts.ML

     | Name name => Pretty.str (prfx "name: " ^ quote name))
   end;
 
 fun pretty_const ctxt (nm, ty) =
   let
-    val ty' = Logic.unvarifyT ty;
+    val ty' = Logic.unvarifyT_global ty;
   in
     Pretty.block
      [Pretty.quote (Pretty.str nm), Pretty.fbrk,
       Pretty.str "::", Pretty.brk 1,
       Pretty.quote (Syntax.pretty_typ ctxt ty')]