diff -r 12cc54fac9b0 -r 53ef7b78e78a src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 16:07:11 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 16:42:17 2015 +0200
@@ -127,8 +127,8 @@
       map (map (rpair [])) asm_propss;
 
     (*obtain params*)
-    val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
-    val params = map Free (xs' ~~ Ts);
+    val (params, params_ctxt) =
+      declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
     val cparams = map (Thm.cterm_of params_ctxt) params;
     val binds' = map (apsnd (fold_rev Term.dependent_lambda_name (xs ~~ params))) binds;
 
@@ -259,7 +259,7 @@
 fun inferred_type (binding, _, mx) ctxt =
   let
     val x = Variable.check_name binding;
-    val (T, ctxt') = Proof_Context.inferred_param x ctxt
+    val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
 fun polymorphic ctxt vars =