# HG changeset patch
# User wenzelm
# Date 1433850178 -7200
# Node ID 422b63ef01474985ce155c551949a84c6f3a4250
# Parent  9be917b2f3767fd4f0d287c57e2ba6f1648ad97f
clarified abstracted term bindings (again, see c8384ff11711);

diff -r 9be917b2f376 -r 422b63ef0147 NEWS
--- a/NEWS	Tue Jun 09 12:32:01 2015 +0200
+++ b/NEWS	Tue Jun 09 13:42:58 2015 +0200
@@ -10,7 +10,7 @@
 *** Pure ***
 
 * Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over the hypothetical parameters.
+the proof body as well, abstracted over relevant parameters.
 
 * New Isar command 'supply' supports fact definitions during goal
 refinement ('apply' scripts).
diff -r 9be917b2f376 -r 422b63ef0147 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Jun 09 12:32:01 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jun 09 13:42:58 2015 +0200
@@ -130,7 +130,7 @@
     val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
     val params = map Free (xs' ~~ Ts);
     val cparams = map (Thm.cterm_of params_ctxt) params;
-    val binds' = map (apsnd (fold_rev Term.lambda_name (xs ~~ params))) binds;
+    val binds' = map (apsnd (fold_rev Term.dependent_lambda_name (xs ~~ params))) binds;
 
     val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
 
diff -r 9be917b2f376 -r 422b63ef0147 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Jun 09 12:32:01 2015 +0200
+++ b/src/Pure/term.ML	Tue Jun 09 13:42:58 2015 +0200
@@ -152,6 +152,7 @@
   val rename_abs: term -> term -> term -> term option
   val is_open: term -> bool
   val is_dependent: term -> bool
+  val dependent_lambda_name: string * term -> term -> term
   val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
@@ -749,6 +750,10 @@
   | term_name (Var ((x, _), _)) = x
   | term_name _ = Name.uu;
 
+fun dependent_lambda_name (x, v) t =
+  let val t' = abstract_over (v, t)
+  in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
+
 fun lambda_name (x, v) t =
   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));