1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Dec 02 22:54:51 2005 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Dec 02 22:54:52 2005 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4    val mark_bound: string -> term
     1.5    val mark_boundT: string * typ -> 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 @@ -107,9 +108,9 @@
    1.12      fun tr (Free (x, T), t) = Lexicon.const name $ Term.absfree (x, T, t)
    1.13        | tr (Const ("_idtdummy", T), t) = Lexicon.const name $ Term.absdummy (T, t)
    1.14        | tr (Const ("_constrain", _) $ Free (x, T) $ tT, t) =
    1.15 -            Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT)
    1.16 +          Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absfree (x, T, t) $ tT)
    1.17        | tr (Const ("_constrain", _) $ Const ("_idtdummy", T) $ tT, t) =
    1.18 -            Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT)
    1.19 +          Lexicon.const name $ (Lexicon.const constrainAbsC $ Term.absdummy (T, t) $ tT)
    1.20        | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
    1.21        | tr (t1, t2) = raise TERM ("binder_tr", [t1, t2]);
    1.22  
    1.23 @@ -479,6 +480,8 @@
    1.24  
    1.25  (** asts_to_terms **)
    1.26  
    1.27 +val fixedN = "\\<^fixed>";
    1.28 +
    1.29  fun asts_to_terms thy trf asts =
    1.30    let
    1.31      fun trans a args =
    1.32 @@ -496,7 +499,15 @@
    1.33            Term.list_comb (term_of ast, map term_of asts)
    1.34        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
    1.35  
    1.36 -    val exn_results = map (capture term_of) asts;
    1.37 +    fun free_fixed (a as Const (c, T)) =
    1.38 +          (case try (unprefix fixedN) c of
    1.39 +            NONE => a
    1.40 +          | SOME x => Free (x, T))
    1.41 +      | free_fixed (Abs (x, T, t)) = Abs (x, T, free_fixed t)
    1.42 +      | free_fixed (t $ u) = free_fixed t $ free_fixed u
    1.43 +      | free_fixed a = a;
    1.44 +
    1.45 +    val exn_results = map (capture (term_of #> free_fixed)) asts;
    1.46      val exns = List.mapPartial get_exn exn_results;
    1.47      val results = List.mapPartial get_result exn_results
    1.48    in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;