1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 10 02:22:54 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 10 02:22:56 2006 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4    val mark_boundT: string * typ -> term
     1.5    val bound_vars: (string * typ) list -> term -> term
     1.6    val variant_abs': string * typ * term -> string * term
     1.7 -  val fixedN: string
     1.8  end;
     1.9  
    1.10  signature SYN_TRANS1 =
    1.11 @@ -487,8 +486,6 @@
    1.12  
    1.13  (** asts_to_terms **)
    1.14  
    1.15 -val fixedN = "\\<^fixed>";
    1.16 -
    1.17  fun asts_to_terms context trf asts =
    1.18    let
    1.19      fun trans a args =
    1.20 @@ -506,13 +503,12 @@
    1.21            Term.list_comb (term_of ast, map term_of asts)
    1.22        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
    1.23  
    1.24 -    fun free_fixed (a as Const (c, T)) =
    1.25 -          (case try (unprefix fixedN) c of
    1.26 -            NONE => a
    1.27 +    val free_fixed = Term.map_aterms
    1.28 +      (fn t as Const (c, T) =>
    1.29 +          (case try (unprefix Lexicon.fixedN) c of
    1.30 +            NONE => t
    1.31            | SOME x => Free (x, T))
    1.32 -      | free_fixed (Abs (x, T, t)) = Abs (x, T, free_fixed t)
    1.33 -      | free_fixed (t $ u) = free_fixed t $ free_fixed u
    1.34 -      | free_fixed a = a;
    1.35 +        | t => t);
    1.36  
    1.37      val exn_results = map (capture (term_of #> free_fixed)) asts;
    1.38      val exns = List.mapPartial get_exn exn_results;