# HG changeset patch
# User wenzelm
# Date 1447420314 -3600
# Node ID f217bbe4e93e5cd2e84e39713c0719516833c8a2
# Parent  4a28eec739e9c1d9ee5cbae1c2bf3d72645a2e06
avoid vacuous quantification, as usual for shared variable scope;

diff -r 4a28eec739e9 -r f217bbe4e93e src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Nov 13 11:41:11 2015 +0100
+++ b/src/Pure/Isar/proof.ML	Fri Nov 13 14:11:54 2015 +0100
@@ -685,7 +685,8 @@
       #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
 
     fun close prop =
-      fold_rev Logic.all_name params (Logic.list_implies (flat prems_propss, prop));
+      fold_rev Logic.dependent_all_name params
+        (Logic.list_implies (flat prems_propss, prop));
     val propss = (map o map) close concl_propss;
   in
     state
diff -r 4a28eec739e9 -r f217bbe4e93e src/Pure/logic.ML
--- a/src/Pure/logic.ML	Fri Nov 13 11:41:11 2015 +0100
+++ b/src/Pure/logic.ML	Fri Nov 13 14:11:54 2015 +0100
@@ -9,7 +9,7 @@
 sig
   val all_const: typ -> term
   val all: term -> term -> term
-  val all_name: string * term -> term -> term
+  val dependent_all_name: string * term -> term -> term
   val is_all: term -> bool
   val dest_all: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
@@ -99,7 +99,13 @@
 fun all_const T = Const ("Pure.all", (T --> propT) --> propT);
 
 fun all v t = all_const (Term.fastype_of v) $ lambda v t;
-fun all_name (x, v) t = all_const (Term.fastype_of v) $ Term.lambda_name (x, v) t;
+
+fun dependent_all_name (x, v) t =
+  let
+    val x' = if x = "" then Term.term_name v else x;
+    val T = Term.fastype_of v;
+    val t' = Term.abstract_over (v, t);
+  in if Term.is_dependent t' then all_const T $ Abs (x', T, t') else t end;
 
 fun is_all (Const ("Pure.all", _) $ Abs _) = true
   | is_all _ = false;
diff -r 4a28eec739e9 -r f217bbe4e93e src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Nov 13 11:41:11 2015 +0100
+++ b/src/Pure/term.ML	Fri Nov 13 14:11:54 2015 +0100
@@ -153,6 +153,7 @@
   val rename_abs: term -> term -> term -> term option
   val is_open: term -> bool
   val is_dependent: term -> bool
+  val term_name: term -> string
   val dependent_lambda_name: string * term -> term -> term
   val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term