--- 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).
--- 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;
--- 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));