# HG changeset patch
# User wenzelm
# Date 1433793855 -7200
# Node ID 599bff6c8c9e0b17670cb8535d30a30f397730de
# Parent  04f92c13ff7ea15c7edcac891af21f68f0dd3c4a
clarified context;

diff -r 04f92c13ff7e -r 599bff6c8c9e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 21:39:16 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 22:04:15 2015 +0200
@@ -113,8 +113,9 @@
     val chain_facts = if can Proof.assert_chain state then Proof.the_facts state else [];
 
     (*obtain vars*)
-    val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
-    val (xs', fix_ctxt) = vars_ctxt |> Proof_Context.add_fixes vars;
+    val ((xs', vars), fix_ctxt) = ctxt
+      |> fold_map prep_var raw_vars
+      |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
     val xs = map (Variable.check_name o #1) vars;
 
     (*obtain asms*)
@@ -122,7 +123,7 @@
     val asm_props = flat asm_propss;
     val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
     val asms =
-      map (fn ((b, raw_atts), _) => (b, map (prep_att ctxt) raw_atts)) raw_asms ~~
+      map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
       map (map (rpair [])) asm_propss;
 
     (*obtain params*)
@@ -137,7 +138,7 @@
 
     (*obtain statements*)
     val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
-    val (thesis_var, thesis) = #1 (bind_judgment fix_ctxt thesisN);
+    val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
 
     val that_name = if name = "" then thatN else name;
     val that_prop =