1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 27 19:55:42 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 27 20:19:05 2011 +0200
     1.3 @@ -1027,15 +1027,16 @@
     1.4  
     1.5  fun add_fixes raw_vars ctxt =
     1.6    let
     1.7 -    val (vars, _) = cert_vars raw_vars ctxt;
     1.8 -    val (xs', ctxt') = Variable.add_fixes (map (Variable.name o #1) vars) ctxt;
     1.9 -    val ctxt'' =
    1.10 -      ctxt'
    1.11 -      |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    1.12 -      |-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
    1.13 -    val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
    1.14 -      Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
    1.15 -  in (xs', ctxt'') end;
    1.16 +    val thy = theory_of ctxt;
    1.17 +    val vars = #1 (cert_vars raw_vars ctxt);
    1.18 +  in
    1.19 +    ctxt
    1.20 +    |> Variable.add_fixes_binding (map #1 vars)
    1.21 +    |-> (fn xs =>
    1.22 +      fold_map declare_var (map2 (fn x => fn (_, T, mx) => (x, T, mx)) xs vars)
    1.23 +      #-> (map_syntax o Local_Syntax.add_syntax thy o map (pair Local_Syntax.Fixed))
    1.24 +      #> pair xs)
    1.25 +  end;
    1.26  
    1.27  
    1.28  (* fixes vs. frees *)