# HG changeset patch
# User wenzelm
# Date 1139534576 -3600
# Node ID 197851f71eef9b53cbcc704ab7a21635b9ec8af8
# Parent  a72c7a1eb1295fea0c69e90cf2fbf1236cfc5480
moved fixedN to lexicon.ML;
tuned;

diff -r a72c7a1eb129 -r 197851f71eef src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 10 02:22:54 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 10 02:22:56 2006 +0100
@@ -22,7 +22,6 @@
   val mark_boundT: string * typ -> term
   val bound_vars: (string * typ) list -> term -> term
   val variant_abs': string * typ * term -> string * term
-  val fixedN: string
 end;
 
 signature SYN_TRANS1 =
@@ -487,8 +486,6 @@
 
 (** asts_to_terms **)
 
-val fixedN = "\\<^fixed>";
-
 fun asts_to_terms context trf asts =
   let
     fun trans a args =
@@ -506,13 +503,12 @@
           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]);
 
-    fun free_fixed (a as Const (c, T)) =
-          (case try (unprefix fixedN) c of
-            NONE => a
+    val free_fixed = Term.map_aterms
+      (fn t as Const (c, T) =>
+          (case try (unprefix Lexicon.fixedN) c of
+            NONE => t
           | SOME x => Free (x, T))
-      | free_fixed (Abs (x, T, t)) = Abs (x, T, free_fixed t)
-      | free_fixed (t $ u) = free_fixed t $ free_fixed u
-      | free_fixed a = a;
+        | t => t);
 
     val exn_results = map (capture (term_of #> free_fixed)) asts;
     val exns = List.mapPartial get_exn exn_results;