# HG changeset patch
# User wenzelm
# Date 1272531632 -7200
# Node ID 586af36cf3cc19642a507dde0be14b8bbf469c89
# Parent  6c7ba330ab42bf28857570273b23198af903d696
uniform decoding of fixed/const syntax entities, allows to pass "\<^fixed>foo__" through the syntax layer (supersedes 1b7109c10b7b);

diff -r 6c7ba330ab42 -r 586af36cf3cc src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Wed Apr 28 19:43:45 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Thu Apr 29 11:00:32 2010 +0200
@@ -567,14 +567,7 @@
           Term.list_comb (term_of ast, map term_of asts)
       | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
 
-    val free_fixed = Term.map_aterms
-      (fn t as Const (c, T) =>
-          (case try Lexicon.unmark_fixed c of
-            NONE => t
-          | SOME x => Free (x, T))
-        | t => t);
-
-    val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
+    val exn_results = map (Exn.capture term_of) asts;
     val exns = map_filter Exn.get_exn exn_results;
     val results = map_filter Exn.get_result exn_results
   in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
diff -r 6c7ba330ab42 -r 586af36cf3cc src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Wed Apr 28 19:43:45 2010 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Thu Apr 29 11:00:32 2010 +0200
@@ -120,11 +120,14 @@
       | decode (Abs (x, T, t)) = Abs (x, T, decode t)
       | decode (t $ u) = decode t $ decode u
       | decode (Const (a, T)) =
-          let val c =
-            (case try Lexicon.unmark_const a of
-              SOME c => c
-            | NONE => snd (map_const a))
-          in Const (c, T) end
+          (case try Lexicon.unmark_fixed a of
+            SOME x => Free (x, T)
+          | NONE =>
+              let val c =
+                (case try Lexicon.unmark_const a of
+                  SOME c => c
+                | NONE => snd (map_const a))
+              in Const (c, T) end)
       | decode (Free (a, T)) =
           (case (map_free a, map_const a) of
             (SOME x, _) => Free (x, T)