src/Pure/Isar/obtain.ML

     val asms =
       map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
       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;
 
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 

   in ((vars', rule''), ctxt') end;
 
 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 =
   let val Ts = map Logic.dest_type (Variable.polymorphic ctxt (map (Logic.mk_type o #2) vars))
   in map2 (fn (x, _, mx) => fn T => ((x, T), mx)) vars Ts end;