defaults for free variables hide consts of same name;

--- a/src/Pure/type.ML	Thu Jun 25 15:20:59 1998 +0200
+++ b/src/Pure/type.ML	Thu Jun 25 15:22:05 1998 +0200
@@ -830,6 +830,7 @@
 fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   let
     fun get_type xi = if_none (def_type xi) dummyT;
+    fun is_free x = is_some (def_type (x, ~1));
     val raw_env = Syntax.raw_term_sorts tm;
     val sort_of = get_sort tsig def_sort map_sort raw_env;
 
@@ -845,7 +846,8 @@
       | decode (t $ u) = decode t $ decode u
       | decode (Free (x, T)) =
           let val c = map_const x in
-            if is_const c orelse NameSpace.qualified c then Const (c, certT T)
+            if not (is_free x) andalso (is_const c orelse NameSpace.qualified c) then
+              Const (c, certT T)
             else if T = dummyT then Free (x, get_type (x, ~1))
             else constrain (Free (x, certT T)) (get_type (x, ~1))
           end