summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 09 Jun 2015 13:42:58 +0200 | |

changeset 60404 | 422b63ef0147 |

parent 60403 | 9be917b2f376 |

child 60405 | 990c9fea6773 |

clarified abstracted term bindings (again, see c8384ff11711);

NEWS | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/obtain.ML | file | annotate | diff | comparison | revisions | |

src/Pure/term.ML | file | annotate | diff | comparison | revisions |

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