diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/Tools/find_consts.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -68,7 +68,7 @@
 
 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,