src/Pure/Isar/proof.ML
changeset 45597 ce23193a42a4
parent 45390 e29521ef9059
child 45666 d83797ef0d2d
     1.1 --- a/src/Pure/Isar/proof.ML	Sun Nov 20 16:58:12 2011 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sun Nov 20 16:59:37 2011 +0100
     1.3 @@ -575,13 +575,13 @@
     1.4  
     1.5  fun gen_fix prep_vars args =
     1.6    assert_forward
     1.7 -  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (prep_vars ctxt args) ctxt))
     1.8 +  #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
     1.9    #> put_facts NONE;
    1.10  
    1.11  in
    1.12  
    1.13 -val fix = gen_fix (K I);
    1.14 -val fix_cmd = gen_fix (fn ctxt => fn args => fst (Proof_Context.read_vars args ctxt));
    1.15 +val fix = gen_fix Proof_Context.cert_vars;
    1.16 +val fix_cmd = gen_fix Proof_Context.read_vars;
    1.17  
    1.18  end;
    1.19