# HG changeset patch # User wenzelm # Date 1321804777 -3600 # Node ID ce23193a42a4f910a295200ede2258c2ca07654d # Parent a27cd85b6028092373e1524947d6cc9a0e69a7f5 uniform cert_vars/read_vars; diff -r a27cd85b6028 -r ce23193a42a4 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sun Nov 20 16:58:12 2011 +0100 +++ b/src/Pure/Isar/proof.ML Sun Nov 20 16:59:37 2011 +0100 @@ -575,13 +575,13 @@ fun gen_fix prep_vars args = assert_forward - #> map_context (fn ctxt => snd (Proof_Context.add_fixes (prep_vars ctxt args) ctxt)) + #> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt)) #> put_facts NONE; in -val fix = gen_fix (K I); -val fix_cmd = gen_fix (fn ctxt => fn args => fst (Proof_Context.read_vars args ctxt)); +val fix = gen_fix Proof_Context.cert_vars; +val fix_cmd = gen_fix Proof_Context.read_vars; end;