# 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;