src/Pure/logic.ML

--- a/src/Pure/logic.ML	Sat Jun 13 15:51:19 2015 +0200
+++ b/src/Pure/logic.ML	Sat Jun 13 16:35:27 2015 +0200
@@ -12,6 +12,8 @@
   val is_all: term -> bool
   val dest_all: term -> (string * typ) * term
   val list_all: (string * typ) list * term -> term
+  val all_constraint: (string -> typ option) -> string * string -> term -> term
+  val dependent_all_constraint: (string -> typ option) -> string * string -> term -> term
   val mk_equals: term * term -> term
   val dest_equals: term -> term * term
   val implies: term
@@ -109,6 +111,35 @@
   | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
 
 
+(* operations before type-inference *)
+
+local
+
+fun abs_body default_type z tm =
+  let
+    fun abs lev (Abs (x, T, b)) = Abs (x, T, abs (lev + 1) b)
+      | abs lev (t $ u) = abs lev t $ abs lev u
+      | abs lev (a as Free (x, T)) =
+          if x = z then
+            Type.constraint (the_default dummyT (default_type x))
+              (Type.constraint T (Bound lev))
+          else a
+      | abs _ a = a;
+  in abs 0 (Term.incr_boundvars 1 tm) end;
+
+in
+
+fun all_constraint default_type (y, z) t =
+  all_const dummyT $ Abs (y, dummyT, abs_body default_type z t);
+
+fun dependent_all_constraint default_type (y, z) t =
+  let val t' = abs_body default_type z t
+  in if Term.is_dependent t' then all_const dummyT $ Abs (y, dummyT, t') else t end;
+
+end;
+
+
+
 (** equality **)
 
 fun mk_equals (t, u) =