# HG changeset patch
# User wenzelm
# Date 898780925 -7200
# Node ID ce093ff0880e356d9bfc9203efba76283ff08293
# Parent  2a8ed71f791ff629cd751f3f18eeeaed12a2a03f
defaults for free variables hide consts of same name;

diff -r 2a8ed71f791f -r ce093ff0880e src/Pure/type.ML
--- 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