clarified abstracted term bindings;

--- a/NEWS	Mon Jun 08 20:58:43 2015 +0200
+++ b/NEWS	Mon Jun 08 21:23:28 2015 +0200
@@ -10,7 +10,7 @@
 *** Pure ***
 
 * Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over hypothetical parameters.
+the proof body as well, abstracted over the hypothetical parameters.
 
 * New Isar command 'supply' supports fact definitions during goal
 refinement ('apply' scripts).

--- a/src/Pure/Isar/obtain.ML	Mon Jun 08 20:58:43 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Mon Jun 08 21:23:28 2015 +0200
@@ -132,13 +132,8 @@
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
     (*abstracted term bindings*)
-    fun abs_params t =
-      let
-        val ps =
-          (xs ~~ params) |> map_filter (fn (x, p) =>
-            if exists_subterm (fn u => u aconv p) t then SOME (x, p) else NONE);
-      in fold_rev Term.lambda_name ps t end;
-    val binds' = map (apsnd (Term.close_schematic_term o abs_params)) binds;
+    val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params);
+    val binds' = map (apsnd abs_term) binds;
 
     (*obtain statements*)
     val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;