--- a/src/Pure/logic.ML Sat Jan 14 19:06:05 2012 +0100
+++ b/src/Pure/logic.ML Sat Jan 14 20:05:58 2012 +0100
@@ -11,6 +11,7 @@
val all: term -> term -> term
val is_all: term -> bool
val dest_all: term -> (string * typ) * term
+ val list_all: (string * typ) list * term -> term
val mk_equals: term * term -> term
val dest_equals: term -> term * term
val implies: term
@@ -104,6 +105,9 @@
in ((x, T), b) end
| dest_all t = raise TERM ("dest_all", [t]);
+fun list_all ([], t) = t
+ | list_all ((a, T) :: vars, t) = all_const T $ Abs (a, T, list_all (vars, t));
+
(** equality **)
@@ -453,8 +457,7 @@
let val params = strip_params A;
val vars = ListPair.zip (Name.variant_list [] (map #1 params),
map #2 params)
- in list_all (vars, remove_params (length vars) n A)
- end;
+ in list_all (vars, remove_params (length vars) n A) end;
(*Makes parameters in a goal have the names supplied by the list cs.*)
fun list_rename_params cs (Const ("==>", _) $ A $ B) =