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;