# HG changeset patch
# User wenzelm
# Date 1433791408 -7200
# Node ID c8384ff11711bdd4b2018355d56636cc5bebaa8a
# Parent  ea3a699964aad19a44bc0ac1f9a78d5da9e21f78
clarified abstracted term bindings;

diff -r ea3a699964aa -r c8384ff11711 NEWS
--- 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).
diff -r ea3a699964aa -r c8384ff11711 src/Pure/Isar/obtain.ML
--- 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;