# HG changeset patch
# User wenzelm
# Date 1433792356 -7200
# Node ID 04f92c13ff7ea15c7edcac891af21f68f0dd3c4a
# Parent  c8384ff11711bdd4b2018355d56636cc5bebaa8a
tuned;

diff -r c8384ff11711 -r 04f92c13ff7e src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 21:23:28 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 21:39:16 2015 +0200
@@ -123,7 +123,7 @@
     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 ~~
-      unflat asm_propss (map (rpair []) asm_props);
+      map (map (rpair [])) asm_propss;
 
     (*obtain params*)
     val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);