# HG changeset patch
# User wenzelm
# Date 1213383884 -7200
# Node ID d1b8b6938b239fb19e27b4ab53632d868e34e202
# Parent  ef2f01da7a127546434306f552bea8dab0ce13db
map_const: soft version, no failure here (recovers hiding of consts, because a hidden name is illegal and rejected later);

diff -r ef2f01da7a12 -r d1b8b6938b23 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Jun 13 21:04:43 2008 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Fri Jun 13 21:04:44 2008 +0200
@@ -12,7 +12,7 @@
   val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
-    (string -> string option) -> (string -> string option) ->
+    (string -> bool * string) -> (string -> string option) ->
     (typ -> typ) -> (sort -> sort) -> term -> term
   val term_of_typ: bool -> typ -> term
   val no_brackets: unit -> bool
@@ -119,13 +119,13 @@
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =
           let val c =
-            (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => perhaps map_const a)
+            (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => snd (map_const a))
           in Const (c, map_type T) end
       | decode (Free (a, T)) =
           (case (map_free a, map_const a) of
             (SOME x, _) => Free (x, map_type T)
-          | (_, SOME c) => Const (c, map_type T)
-          | _ => (if NameSpace.is_qualified a then Const else Free) (a, map_type T))
+          | (_, (true, c)) => Const (c, map_type T)
+          | (_, (false, c)) => (if NameSpace.is_qualified c then Const else Free) (c, map_type T))
       | decode (Var (xi, T)) = Var (xi, map_type T)
       | decode (t as Bound _) = t;
   in decode tm end;