1.1 --- a/src/Pure/Isar/proof.ML	Sat Mar 28 17:21:49 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Mar 28 17:53:33 2009 +0100
     1.3 @@ -531,15 +531,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun gen_fix add_fixes args =
     1.8 +fun gen_fix prep_vars args =
     1.9    assert_forward
    1.10 -  #> map_context (snd o add_fixes args)
    1.11 +  #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
    1.12    #> put_facts NONE;
    1.13  
    1.14  in
    1.15  
    1.16 -val fix = gen_fix ProofContext.add_fixes;
    1.17 -val fix_i = gen_fix ProofContext.add_fixes_i;
    1.18 +val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
    1.19 +val fix_i = gen_fix (K I);
    1.20  
    1.21  end;
    1.22